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
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 ) )
A2: the carrier of S = the carrier of (Omega S) by Lm1;
the carrier of T = the carrier of (Omega T) by Lm1;
then reconsider f = h as Function of (Omega S),(Omega T) by A2;
A3: f is isomorphic by A1, Th18;
A4: f " is isomorphic by A1, Th18, YELLOW14:11;
A5: rng f = the carrier of (Omega T) by A3, WAYBEL_0:66;
A6: ( rng h = [#] T & h is one-to-one ) by A1, TOPS_2:def 5;
f " is monotone by A4;
then (f " ) .: D is directed by YELLOW_2:17;
then A7: f " D is non empty directed Subset of (Omega S) by A5, A6, TOPS_2:68;
then ex_sup_of f " D, Omega S by Def4;
then ex_sup_of f .: (f " D), Omega T by A1, Th18, YELLOW14:17;
hence A8: ex_sup_of D, Omega T by A5, FUNCT_1:147; :: 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 )
A9: h " V is open by A1, TOPGRP_1:26;
f " is sups-preserving by A4, WAYBEL13:20;
then A10: f " preserves_sup_of D by WAYBEL_0:def 33;
assume sup D in V ; :: thesis: D meets V
then (h " ) . (sup D) in (h " ) .: V by FUNCT_2:43;
then (h " ) . (sup D) in h " V by A6, TOPS_2:68;
then (h " ) . (sup D) in h " V by A6, TOPS_2:def 4;
then (f " ) . (sup D) in h " V by A5, A6, TOPS_2:def 4;
then sup ((f " ) .: D) in h " V by A8, A10, WAYBEL_0:def 31;
then sup (f " D) in h " V by A5, A6, TOPS_2:68;
then f " D meets h " V by A7, A9, Def4;
then consider a being set such that
A11: ( a in f " D & a in h " V ) by XBOOLE_0:3;
reconsider a = a as Element of S by A11;

now

take b = h . a; :: thesis: ( b in D & b in V )
thus ( b in D & b in V ) by A11, FUNCT_2:46; :: thesis: verum

end;

hence D meets V by XBOOLE_0:3; :: thesis: verum