let S be monotone-convergence T_0-TopSpace; :: thesis: for T being T_0-TopSpace st S,T are_homeomorphic holds
T is monotone-convergence
let T be T_0-TopSpace; :: thesis: ( S,T are_homeomorphic implies T is monotone-convergence )
given h being Function of S,T such that A1: h is being_homeomorphism ; :: according to T_0TOPSP:def 1 :: thesis: T is monotone-convergence
the carrier of S = the carrier of (Omega S) by Lm1;
then reconsider f = h as Function of (Omega S),(Omega T) by Lm1;
f is isomorphic by A1, Th18;
then A2: rng f = the carrier of (Omega T) by WAYBEL_0:66;
let D be non empty directed Subset of (Omega T); :: according to WAYBEL25:def 4 :: thesis: ( ex_sup_of D, Omega T & ( for V being open Subset of T st sup D in V holds
D meets V ) )
A3: f " is isomorphic by A1, Th18, YELLOW14:10;
then f " is sups-preserving by WAYBEL13:20;
then A4: f " preserves_sup_of D ;
A5: rng h = [#] T by A1;
A6: h is V7() by A1;
A7: h is onto by A5, FUNCT_2:def 3;
(f ") .: D is directed by A3, YELLOW_2:15;
then A8: f " D is non empty directed Subset of (Omega S) by A2, A5, A6, TOPS_2:55;
then ex_sup_of f " D, Omega S by Def4;
then ex_sup_of f .: (f " D), Omega T by A1, Th18, YELLOW14:16;
hence A9: ex_sup_of D, Omega T by A2, FUNCT_1:77; :: thesis: for V being open Subset of T st sup D in V holds
D meets V
let V be open Subset of T; :: thesis: ( sup D in V implies D meets V )
assume sup D in V ; :: thesis: D meets V
then (h ") . (sup D) in (h ") .: V by FUNCT_2:35;
then (h ") . (sup D) in h " V by A5, A6, TOPS_2:55;
then (h ") . (sup D) in h " V by A7, A6, TOPS_2:def 4;
then (f ") . (sup D) in h " V by A2, A6, A7, A5, TOPS_2:def 4;
then sup ((f ") .: D) in h " V by A9, A4;
then A10: sup (f " D) in h " V by A2, A5, A6, TOPS_2:55;
h " V is open by A1, TOPGRP_1:26;
then f " D meets h " V by A8, A10, Def4;
then consider a being object such that
A11: a in f " D and
A12: a in h " V by XBOOLE_0:3;
reconsider a = a as Element of S by A12;
hence D meets V by XBOOLE_0:3; :: thesis: verum