reconsider B1 = BoolePoset {0} 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 {0}))
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 {0})) by A1, A2, Th25 ; :: thesis: verum