reconsider B1 = BoolePoset 1 as complete LATTICE ;
reconsider OSS = Omega Sierpinski_Space as complete Scott TopAugmentation of B1 by Th31, WAYBEL26:4;
let S be complete Scott TopLattice; :: thesis: oContMaps S,Sierpinski_Space = UPS S,(BoolePoset 1)
A1: RelStr(# the carrier of S,the InternalRel of S #) = RelStr(# the carrier of S,the InternalRel of S #) ;
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 A2: 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, A2, Th25 ; :: thesis: verum