let S be complete Scott TopLattice; :: thesis: Omega S = TopRelStr(# the carrier of S, the InternalRel of S, the topology of S #)
A1: TopStruct(# the carrier of (Omega S), the topology of (Omega S) #) = TopStruct(# the carrier of S, the topology of S #) by Def2;
the InternalRel of (Omega S) = the InternalRel of S
proof
let x, y be object ; :: according to RELAT_1:def 2 :: thesis: ( ( not [x,y] in the InternalRel of (Omega S) or [x,y] in the InternalRel of S ) & ( not [x,y] in the InternalRel of S or [x,y] in the InternalRel of (Omega S) ) )
hereby :: thesis: ( not [x,y] in the InternalRel of S or [x,y] in the InternalRel of (Omega S) )
assume A2: [x,y] in the InternalRel of (Omega S) ; :: thesis: [x,y] in the InternalRel of S
then A3: y in the carrier of (Omega S) by ZFMISC_1:87;
x in the carrier of (Omega S) by A2, ZFMISC_1:87;
then reconsider t1 = x, t2 = y as Element of S by A3, Lm1;
reconsider o1 = x, o2 = y as Element of (Omega S) by A2, ZFMISC_1:87;
o1 <= o2 by A2;
then ex Y2 being Subset of S st
( Y2 = {o2} & o1 in Cl Y2 ) by Def2;
then t1 in downarrow t2 by WAYBEL11:9;
then ex t3 being Element of S st
( t3 >= t1 & t3 in {t2} ) by WAYBEL_0:def 15;
then t1 <= t2 by TARSKI:def 1;
hence [x,y] in the InternalRel of S ; :: thesis: verum
end;
assume A4: [x,y] in the InternalRel of S ; :: thesis: [x,y] in the InternalRel of (Omega S)
then reconsider t1 = x, t2 = y as Element of S by ZFMISC_1:87;
reconsider o1 = x, o2 = y as Element of (Omega S) by A1, A4, ZFMISC_1:87;
A5: t2 in {t2} by TARSKI:def 1;
t1 <= t2 by A4;
then t1 in downarrow t2 by A5, WAYBEL_0:def 15;
then t1 in Cl {t2} by WAYBEL11:9;
then o1 <= o2 by Def2;
hence [x,y] in the InternalRel of (Omega S) ; :: thesis: verum
end;
hence Omega S = TopRelStr(# the carrier of S, the InternalRel of S, the topology of S #) by A1; :: thesis: verum