Prove that strongly dense maps are closed under pullbacks along open maps

This is [Topology.Locale/pullback_sdense](https://github.com/JetBrains/arend-lib/blob/4ea97da483c5bb2e6a22c8d09c03becf17756c7e/src/Topology/Locale.ard#L1182). A proof of this lemma can be found in A constructive “Closed subgroup theorem” for localic groups and groupoids, Peter T. Johnstone, 1989, Lemma 1.9.

Open src/Topology/Locale.ard at the Topology.Locale/pullback_sdense lemma. Read the surrounding definitions and compare the statement with Lemma 1.9 of Peter T. Johnstone's 1989 paper. Done means the strongly dense maps result is formally proved in the Arend library.

Written by the indexing model from the issue text.