let Z be monotone-convergence T_0-TopSpace; :: thesis: for Y being non empty SubSpace of Z
for f being continuous Function of Z,Y st f is being_a_retraction holds
Omega Y is directed-sups-inheriting SubRelStr of Omega Z
let Y be non empty SubSpace of Z; :: thesis: for f being continuous Function of Z,Y st f is being_a_retraction holds
Omega Y is directed-sups-inheriting SubRelStr of Omega Z
reconsider OZ = Omega Z as non empty up-complete Poset ;
reconsider OY = Omega Y as non empty full SubRelStr of Omega Z by WAYBEL25:17;
let f be continuous Function of Z,Y; :: thesis: ( f is being_a_retraction implies Omega Y is directed-sups-inheriting SubRelStr of Omega Z )
assume A1: f is being_a_retraction ; :: thesis: Omega Y is directed-sups-inheriting SubRelStr of Omega Z
A2: ( dom f = the carrier of Z & rng f c= the carrier of Y ) by FUNCT_2:def 1;
( [#] Y c= [#] Z & [#] Y = the carrier of Y & [#] Z = the carrier of Z ) by PRE_TOPC:def 9;
then rng f c= the carrier of Z by XBOOLE_1:1;
then A3: f is continuous Function of Z,Z by A2, PRE_TOPC:56, RELSET_1:11;
TopStruct(# the carrier of (Omega Z),the topology of (Omega Z) #) = TopStruct(# the carrier of Z,the topology of Z #) by WAYBEL25:def 2;
then reconsider f' = f as continuous Function of (Omega Z),(Omega Z) by A3, YELLOW12:36;
reconsider g = f' as Function of OZ,OZ ;
( g is idempotent & g is directed-sups-preserving ) by A1, YELLOW16:47;
then A4: Image g is directed-sups-inheriting by YELLOW16:6;
A5: ( TopStruct(# the carrier of (Omega Y),the topology of (Omega Y) #) = TopStruct(# the carrier of Y,the topology of Y #) & TopStruct(# the carrier of (Omega Z),the topology of (Omega Z) #) = TopStruct(# the carrier of Z,the topology of Z #) ) by WAYBEL25:def 2;
A6: ( Image g = subrelstr (rng g) & rng g = the carrier of (subrelstr (rng g)) ) by YELLOW_0:def 15;
RelStr(# the carrier of OZ,the InternalRel of OZ #) = RelStr(# the carrier of (Omega Z),the InternalRel of (Omega Z) #) ;
then OY is directed-sups-inheriting by A1, A4, A5, A6, WAYBEL21:22, YELLOW16:46;
hence Omega Y is directed-sups-inheriting SubRelStr of Omega Z ; :: thesis: verum