set SS = Sierpinski_Space ;
set B = BoolePoset 1;
let T be injective T_0-TopSpace; :: thesis: for S being Scott TopAugmentation of Omega T holds TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #)
let S be Scott TopAugmentation of Omega T; :: thesis: TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #)
consider M being non empty set such that
A1: T is_Retract_of product (M --> Sierpinski_Space) by WAYBEL18:20;
consider c being continuous Function of T,(product (M --> Sierpinski_Space)), r being continuous Function of (product (M --> Sierpinski_Space)),T such that
A2: r * c = id T by A1, Def1;
A3: TopStruct(# the carrier of T, the topology of T #) = TopStruct(# the carrier of (Omega T), the topology of (Omega T) #) by Def2;
A4: TopStruct(# the carrier of (product (M --> Sierpinski_Space)), the topology of (product (M --> Sierpinski_Space)) #) = TopStruct(# the carrier of (Omega (product (M --> Sierpinski_Space))), the topology of (Omega (product (M --> Sierpinski_Space))) #) by Def2;
then reconsider c1a = c as Function of (Omega T),(Omega (product (M --> Sierpinski_Space))) by A3;
consider S2M being Scott TopAugmentation of product (M --> (BoolePoset 1));
A5: TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of S, the topology of S #) ;
A6: RelStr(# the carrier of S2M, the InternalRel of S2M #) = RelStr(# the carrier of (product (M --> (BoolePoset 1))), the InternalRel of (product (M --> (BoolePoset 1))) #) by YELLOW_9:def 4;
then reconsider c1 = c as Function of (Omega T),(product (M --> (BoolePoset 1))) by A3, Th3;
A7: RelStr(# the carrier of S, the InternalRel of S #) = RelStr(# the carrier of (Omega T), the InternalRel of (Omega T) #) by YELLOW_9:def 4;
then reconsider c2 = c1 as Function of S,S2M by A6;
A8: the carrier of S2M = the carrier of (product (M --> Sierpinski_Space)) by Th3;
then reconsider rr = r as Function of S2M,T ;
A9: the topology of S2M = the topology of (product (M --> Sierpinski_Space)) by WAYBEL18:16;
then reconsider W = T as non empty monotone-convergence TopSpace by A1, A8, Th36;
Omega (product (M --> Sierpinski_Space)) = Omega S2M by A9, A8, Th13;
then A10: RelStr(# the carrier of (Omega (product (M --> Sierpinski_Space))), the InternalRel of (Omega (product (M --> Sierpinski_Space))) #) = RelStr(# the carrier of (product (M --> (BoolePoset 1))), the InternalRel of (product (M --> (BoolePoset 1))) #) by Th16
.= RelStr(# the carrier of S2M, the InternalRel of S2M #) by YELLOW_9:def 4 ;
reconsider r1 = r as Function of (product (M --> (BoolePoset 1))),(Omega T) by A8, A6, A3;
A11: RelStr(# the carrier of (Omega S2M), the InternalRel of (Omega S2M) #) = RelStr(# the carrier of (product (M --> (BoolePoset 1))), the InternalRel of (product (M --> (BoolePoset 1))) #) by Th16;
then reconsider rr1 = r1 as Function of (Omega S2M),(Omega T) ;
reconsider r2 = r1 as Function of S2M,S by A6, A7;
reconsider r3 = r2 as Function of (product (M --> Sierpinski_Space)),S by Th3;
TopStruct(# the carrier of (Omega S2M), the topology of (Omega S2M) #) = TopStruct(# the carrier of S2M, the topology of S2M #) by Def2;
then rr1 is continuous by A9, A8, A3, YELLOW12:36;
then r2 is directed-sups-preserving by A6, A7, A11, WAYBEL21:6;
then r3 is continuous by A9, A8, A5, YELLOW12:36;
then A12: r3 * c is continuous ;
reconsider c1a = c1a as continuous Function of (Omega W),(Omega (product (M --> Sierpinski_Space))) by A3, A4, YELLOW12:36;
c2 = c1a ;
then A13: c2 is directed-sups-preserving by A7, A10, WAYBEL21:6;
TopStruct(# the carrier of T, the topology of T #) = TopStruct(# the carrier of T, the topology of T #) ;
then rr is continuous by A9, A8, YELLOW12:36;
then rr * c2 is continuous by A13;
hence TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) by A2, A12, YELLOW14:34; :: thesis: verum