let T be injective T_0-TopSpace; Omega T is complete continuous LATTICE
set S = Sierpinski_Space ;
set B = BoolePoset {0};
consider M being non empty set such that
A1:
T is_Retract_of product (M --> Sierpinski_Space)
by WAYBEL18:19;
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;
A5:
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 A6:
RelStr(# the carrier of (Omega (Image f)), the InternalRel of (Omega (Image f)) #), Omega T are_isomorphic
by A5, WAYBEL_1:7;
Omega (Image f) is full SubRelStr of Omega (product (M --> Sierpinski_Space))
by Th17;
then A7:
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;
set TL = the Scott TopAugmentation of product (M --> (BoolePoset {0}));
A8:
RelStr(# the carrier of the Scott TopAugmentation of product (M --> (BoolePoset {0})), the InternalRel of the Scott TopAugmentation of product (M --> (BoolePoset {0})) #) = RelStr(# the carrier of (product (M --> (BoolePoset {0}))), the InternalRel of (product (M --> (BoolePoset {0}))) #)
by YELLOW_9:def 4;
A9:
the carrier of the Scott TopAugmentation of product (M --> (BoolePoset {0})) = the carrier of (product (M --> Sierpinski_Space))
by Th3;
then reconsider ff = f as Function of the Scott TopAugmentation of product (M --> (BoolePoset {0})), the Scott TopAugmentation of product (M --> (BoolePoset {0})) ;
A10:
the topology of the Scott TopAugmentation of product (M --> (BoolePoset {0})) = the topology of (product (M --> Sierpinski_Space))
by WAYBEL18:15;
then A11:
ff is continuous
by A2, A9, YELLOW12:36;
then
( ff is idempotent & ff is monotone )
by A3, QUANTAL1:def 9;
then
ff is projection
;
then reconsider g = ff as projection Function of (product (M --> (BoolePoset {0}))),(product (M --> (BoolePoset {0}))) by A8, Lm3;
A12:
the InternalRel of (Image g) = the InternalRel of (product (M --> (BoolePoset {0}))) |_2 the carrier of (Image g)
by YELLOW_0:def 14;
( TopStruct(# the carrier of TopStruct(# the carrier of the Scott TopAugmentation of product (M --> (BoolePoset {0})), the topology of the Scott TopAugmentation of product (M --> (BoolePoset {0})) #), the topology of TopStruct(# the carrier of the Scott TopAugmentation of product (M --> (BoolePoset {0})), the topology of the Scott TopAugmentation of product (M --> (BoolePoset {0})) #) #) = TopStruct(# the carrier of the Scott TopAugmentation of product (M --> (BoolePoset {0})), the topology of the Scott TopAugmentation of product (M --> (BoolePoset {0})) #) implies Omega TopStruct(# the carrier of the Scott TopAugmentation of product (M --> (BoolePoset {0})), the topology of the Scott TopAugmentation of product (M --> (BoolePoset {0})) #) = Omega the Scott TopAugmentation of product (M --> (BoolePoset {0})) )
by Th13;
then A13:
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 {0}))), the InternalRel of (product (M --> (BoolePoset {0}))) #)
by A10, A9, Th16;
g is directed-sups-preserving
by A8, A11, WAYBEL21:6;
then A14:
Image g is complete continuous LATTICE
by WAYBEL15:15, YELLOW_2:35;
the carrier of (Image g) =
rng g
by YELLOW_0:def 15
.=
the carrier of (Image f)
by WAYBEL18:9
.=
the carrier of (Omega (Image f))
by Lm1
;
hence
Omega T is complete continuous LATTICE
by A13, A14, A6, A12, A7, WAYBEL15:9, WAYBEL20:18, YELLOW14:11, YELLOW14:12; verum