let S, T be non empty TopSpace; :: thesis: ( TopStruct(# the carrier of S,the topology of S #) = TopStruct(# the carrier of T,the topology of T #) & S is monotone-convergence implies T is monotone-convergence )
assume that
A1: TopStruct(# the carrier of S,the topology of S #) = TopStruct(# the carrier of T,the topology of T #) and
A2: for D being non empty directed Subset of (Omega S) holds
( ex_sup_of D, Omega S & ( for V being open Subset of S st sup D in V holds
D meets V ) ) ; :: according to WAYBEL25:def 4 :: thesis: T is monotone-convergence
let E be non empty directed Subset of (Omega T); :: according to WAYBEL25:def 4 :: thesis: ( ex_sup_of E, Omega T & ( for V being open Subset of T st sup E in V holds
E meets V ) )
A3: Omega S = Omega T by A1, Th13;
hence ex_sup_of E, Omega T by A2; :: thesis: for V being open Subset of T st sup E in V holds
E meets V
let V be open Subset of T; :: thesis: ( sup E in V implies E meets V )
assume A4: sup E in V ; :: thesis: E meets V
reconsider W = V as Subset of S by A1;
reconsider D = E as Subset of (Omega S) by A1, Th13;
( W is open & sup D in W ) by A1, A4, Th13, TOPS_3:76;
hence E meets V by A2, A3; :: thesis: verum