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 #)
set SS = Sierpinski_Space ;
set B = BoolePoset 1;
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;
consider S2M being Scott TopAugmentation of product (M --> (BoolePoset 1));
A3: the topology of S2M = the topology of (product (M --> Sierpinski_Space )) by WAYBEL18:16;
A4: the carrier of S2M = the carrier of (product (M --> Sierpinski_Space )) by Th3;
then reconsider rr = r as Function of S2M,T ;
A5: 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;
A6: TopStruct(# the carrier of T,the topology of T #) = TopStruct(# the carrier of (Omega T),the topology of (Omega T) #) by Def2;
then reconsider r1 = r as Function of (product (M --> (BoolePoset 1))),(Omega T) by A4, A5;
reconsider c1 = c as Function of (Omega T),(product (M --> (BoolePoset 1))) by A4, A5, A6;
A7: 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 A6;
A8: 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 r2 = r1 as Function of S2M,S by A5;
reconsider c2 = c1 as Function of S,S2M by A5, A8;
A9: 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) ;
TopStruct(# the carrier of T,the topology of T #) = TopStruct(# the carrier of T,the topology of T #) ;
then A11: rr is continuous by A3, A4, YELLOW12:36;
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 A3, A4, A6, YELLOW12:36;
then rr1 is directed-sups-preserving ;
then r2 is directed-sups-preserving by A5, A8, A9, WAYBEL21:6;
then A12: r2 is continuous ;
reconsider r3 = r2 as Function of (product (M --> Sierpinski_Space )),S by A4;
TopStruct(# the carrier of S,the topology of S #) = TopStruct(# the carrier of S,the topology of S #) ;
then A13: r3 is continuous by A3, A4, A12, YELLOW12:36;
reconsider W = T as non empty monotone-convergence TopSpace by A1, A3, A4, Th36;
reconsider c1a = c1a as continuous Function of (Omega W),(Omega (product (M --> Sierpinski_Space ))) by A6, A7, YELLOW12:36;
Omega (product (M --> Sierpinski_Space )) = Omega S2M by A3, A4, Th13;
then A14: 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 ;
c2 = c1a ;
then c2 is directed-sups-preserving by A8, A14, WAYBEL21:6;
then c2 is continuous ;
then ( r3 * c is continuous & rr * c2 is continuous ) by A11, A13;
hence TopStruct(# the carrier of S,the topology of S #) = TopStruct(# the carrier of T,the topology of T #) by A2, YELLOW14:34; :: thesis: verum