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; 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
; verum