Prove that a weakly regular locale is weakly Hausdorff

[valis]

This is Topology.Locale/wregular_wHausdorff. A proof of this proposition can be found in Fibrewise separation axioms for locales, Peter T. Johnstone, 1990, Corollary 3.4.

This proposition requires a lot of background work since this paper is not formalized yet and it seems a lot of stuff from it is required for this proof.