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 4;

then ( dom f = the carrier of Z & rng f c= the carrier of Z ) by FUNCT_2:def 1;

then A2: f is continuous Function of Z,Z by PRE_TOPC:26, RELSET_1:4;

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:45;

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:44;

hence Omega Y is directed-sups-inheriting SubRelStr of Omega Z ; :: thesis: verum

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 4;

then ( dom f = the carrier of Z & rng f c= the carrier of Z ) by FUNCT_2:def 1;

then A2: f is continuous Function of Z,Z by PRE_TOPC:26, RELSET_1:4;

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:45;

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:44;

hence Omega Y is directed-sups-inheriting SubRelStr of Omega Z ; :: thesis: verum