let S be complete Scott TopLattice; :: thesis: oContMaps S,Sierpinski_Space = UPS S,(BoolePoset 1)
reconsider B1 = BoolePoset 1 as complete LATTICE ;
reconsider OSS = Omega Sierpinski_Space as complete Scott TopAugmentation of B1 by Th31, WAYBEL26:4;
TopStruct(# the carrier of OSS,the topology of OSS #) = TopStruct(# the carrier of Sierpinski_Space ,the topology of Sierpinski_Space #) by WAYBEL25:def 2;
then Omega OSS = OSS by WAYBEL25:13;
then A1: ( RelStr(# the carrier of S,the InternalRel of S #) = RelStr(# the carrier of S,the InternalRel of S #) & RelStr(# the carrier of OSS,the InternalRel of OSS #) = RelStr(# the carrier of B1,the InternalRel of B1 #) ) by WAYBEL25:16;
thus oContMaps S,Sierpinski_Space = ContMaps S,(Omega Sierpinski_Space ) by WAYBEL26:def 1
.= SCMaps S,OSS by WAYBEL24:38
.= UPS S,OSS by Th24
.= UPS S,(BoolePoset 1) by A1, Th25 ; :: thesis: verum