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 )
A1: RelStr(# the carrier of OZ,the InternalRel of OZ #) = RelStr(# the carrier of (Omega Z),the InternalRel of (Omega Z) #) ;
[#] Y c= [#] Z by PRE_TOPC:def 9;
then ( dom f = the carrier of Z & rng f c= the carrier of Z ) by FUNCT_2:def 1, XBOOLE_1:1;
then A2: f is continuous Function of Z,Z by 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 f9 = f as continuous Function of (Omega Z),(Omega Z) by A2, YELLOW12:36;
reconsider g = f9 as Function of OZ,OZ ;
assume A3: f is being_a_retraction ; :: thesis: Omega Y is directed-sups-inheriting SubRelStr of Omega Z
then ( g is idempotent & g is directed-sups-preserving ) by YELLOW16:47;
then A4: Image g is directed-sups-inheriting by YELLOW16:6;
( TopStruct(# the carrier of (Omega Y),the topology of (Omega Y) #) = TopStruct(# the carrier of Y,the topology of Y #) & rng g = the carrier of (subrelstr (rng g)) ) by WAYBEL25:def 2, YELLOW_0:def 15;
then OY is directed-sups-inheriting by A3, A4, A1, WAYBEL21:22, YELLOW16:46;
hence Omega Y is directed-sups-inheriting SubRelStr of Omega Z ; :: thesis: verum