set S = Sierpinski_Space ;
set B = BoolePoset 1;
let T be injective T_0-TopSpace; :: thesis: Omega T is complete continuous LATTICE
consider M being non empty set such that
A1: T is_Retract_of product (M --> Sierpinski_Space ) by WAYBEL18:20;
consider f being Function of (product (M --> Sierpinski_Space )),(product (M --> Sierpinski_Space )) such that
A2: f is continuous and
A3: f * f = f and
A4: Image f,T are_homeomorphic by A1, WAYBEL18:def 8;
consider TL being Scott TopAugmentation of product (M --> (BoolePoset 1));
A5: the topology of TL = the topology of (product (M --> Sierpinski_Space )) by WAYBEL18:16;
A6: RelStr(# the carrier of TL,the InternalRel of TL #) = RelStr(# the carrier of (product (M --> (BoolePoset 1))),the InternalRel of (product (M --> (BoolePoset 1))) #) by YELLOW_9:def 4;
A7: the carrier of TL = the carrier of (product (M --> Sierpinski_Space )) by Th3;
then reconsider ff = f as Function of TL,TL ;
( TopStruct(# the carrier of TopStruct(# the carrier of TL,the topology of TL #),the topology of TopStruct(# the carrier of TL,the topology of TL #) #) = TopStruct(# the carrier of TL,the topology of TL #) implies Omega TopStruct(# the carrier of TL,the topology of TL #) = Omega TL ) by Th13;
then A8: RelStr(# the carrier of (Omega TopStruct(# the carrier of (product (M --> Sierpinski_Space )),the topology of (product (M --> Sierpinski_Space )) #)),the InternalRel of (Omega TopStruct(# the carrier of (product (M --> Sierpinski_Space )),the topology of (product (M --> Sierpinski_Space )) #)) #) = RelStr(# the carrier of (product (M --> (BoolePoset 1))),the InternalRel of (product (M --> (BoolePoset 1))) #) by A5, A7, Th16;
ff is continuous by A2, A5, A7, YELLOW12:36;
then A9: ff is directed-sups-preserving ;
ff is projection

proof

thus ( ff is idempotent & ff is monotone ) by A3, A9, QUANTAL1:def 9; :: according to WAYBEL_1:def 13 :: thesis: verum

end;

then reconsider g = ff as projection Function of (product (M --> (BoolePoset 1))),(product (M --> (BoolePoset 1))) by A6, Lm3;
g is directed-sups-preserving by A6, A9, WAYBEL21:6;
then A10: Image g is complete continuous LATTICE by WAYBEL15:17, YELLOW_2:37;
A11: RelStr(# the carrier of (Omega (Image f)),the InternalRel of (Omega (Image f)) #), Omega (Image f) are_isomorphic by WAYBEL13:26;
Omega (Image f), Omega T are_isomorphic by A4, Th19;
then A12: RelStr(# the carrier of (Omega (Image f)),the InternalRel of (Omega (Image f)) #), Omega T are_isomorphic by A11, WAYBEL_1:8;
A13: the carrier of (Image g) = rng g by YELLOW_0:def 15
.= the carrier of (Image f) by WAYBEL18:10
.= the carrier of (Omega (Image f)) by Lm1 ;
A14: the InternalRel of (Image g) = the InternalRel of (product (M --> (BoolePoset 1))) |_2 the carrier of (Image g) by YELLOW_0:def 14;
Omega (Image f) is full SubRelStr of Omega (product (M --> Sierpinski_Space )) by Th17;
then the InternalRel of (Omega (Image f)) = the InternalRel of (Omega (product (M --> Sierpinski_Space ))) |_2 the carrier of (Omega (Image f)) by YELLOW_0:def 14;
hence Omega T is complete continuous LATTICE by A8, A10, A12, A13, A14, WAYBEL15:11, WAYBEL20:18, YELLOW14:12, YELLOW14:13; :: thesis: verum