let T be monotone-convergence T_0-TopSpace; :: thesis: for R being T_0-TopSpace st R is_Retract_of T holds
R is monotone-convergence
let R be T_0-TopSpace; :: thesis: ( R is_Retract_of T implies R is monotone-convergence )
given c being continuous Function of R,T, r being continuous Function of T,R such that A1: r * c = id R ; :: according to WAYBEL25:def 1 :: thesis: R is monotone-convergence
let D be non empty directed Subset of (Omega R); :: according to WAYBEL25:def 4 :: thesis: ( ex_sup_of D, Omega R & ( for V being open Subset of R st sup D in V holds
D meets V ) )
A2: TopStruct(# the carrier of T,the topology of T #) = TopStruct(# the carrier of (Omega T),the topology of (Omega T) #) by Def2;
A3: TopStruct(# the carrier of R,the topology of R #) = TopStruct(# the carrier of (Omega R),the topology of (Omega R) #) by Def2;
then reconsider DR = D as non empty Subset of R ;
reconsider f = c * r as Function of (Omega T),(Omega T) by A2;
reconsider cc = c as Function of (Omega R),(Omega T) by A2, A3;
reconsider rr = r as Function of (Omega T),(Omega R) by A2, A3;
cc is continuous by A2, A3, YELLOW12:36;
then cc is monotone ;
then A4: cc .: D is directed by YELLOW_2:17;
then A5: ex_sup_of cc .: D, Omega T by Def4;
A6: r .: (c .: D) = (r * c) .: DR by RELAT_1:159
.= D by A1, FUNCT_1:162 ;
rr is continuous by A2, A3, YELLOW12:36;
then rr is directed-sups-preserving ;
then A7: rr preserves_sup_of cc .: D by A4, WAYBEL_0:def 37;
hence ex_sup_of D, Omega R by A5, A6, WAYBEL_0:def 31; :: thesis: for V being open Subset of R st sup D in V holds
D meets V
let V be open Subset of R; :: thesis: ( sup D in V implies D meets V )
assume A8: sup D in V ; :: thesis: D meets V
A9: c .: V c= r " V

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in c .: V or a in r " V )
assume a in c .: V ; :: thesis: a in r " V
then consider x being set such that
A10: x in the carrier of R and
A11: x in V and
A12: a = c . x by FUNCT_2:115;
reconsider x = x as Point of R by A10;
A13: a = c . x by A12;
r . a = (r * c) . x by A12, FUNCT_2:21
.= x by A1, FUNCT_1:35 ;
hence a in r " V by A11, A13, FUNCT_2:46; :: thesis: verum

end;

[#] R <> {} ;
then A14: r " V is open by TOPS_2:55;
f is continuous by A2, YELLOW12:36;
then f is directed-sups-preserving ;
then A15: f preserves_sup_of cc .: D by A4, WAYBEL_0:def 37;
A16: c . (sup D) = c . (r . (sup (cc .: D))) by A5, A6, A7, WAYBEL_0:def 31
.= f . (sup (cc .: D)) by A2, FUNCT_2:21
.= sup (f .: (cc .: D)) by A5, A15, WAYBEL_0:def 31
.= sup (cc .: D) by A6, RELAT_1:159 ;
c . (sup D) in c .: V by A8, FUNCT_2:43;
then c .: D meets r " V by A4, A9, A14, A16, Def4;
then consider d being set such that
A17: d in cc .: D and
A18: d in r " V by XBOOLE_0:3;

now

take a = r . d; :: thesis: ( a in D & a in V )
thus a in D by A6, A17, FUNCT_2:43; :: thesis: a in V
thus a in V by A18, FUNCT_2:46; :: thesis: verum

end;

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