let S be complete Scott TopLattice; :: thesis: Omega S = TopRelStr(# the carrier of S,the InternalRel of S,the topology of S #)
consider L being Scott TopAugmentation 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
set ;
:: 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 Sthen A3:
(
x in the
carrier of
(Omega S) &
y in the
carrier of
(Omega S) )
by ZFMISC_1:106;
reconsider o1 =
x,
o2 =
y as
Element of
(Omega S) by A2, ZFMISC_1:106;
o1 <= o2
by A2, ORDERS_2:def 9;
then consider Y2 being
Subset of
S such that A4:
(
Y2 = {o2} &
o1 in Cl Y2 )
by Def2;
reconsider t1 =
x,
t2 =
y as
Element of
S by A3, Lm1;
t1 in downarrow t2
by A4, WAYBEL11:9;
then consider t3 being
Element of
S such that A5:
(
t3 >= t1 &
t3 in {t2} )
by WAYBEL_0:def 15;
t1 <= t2
by A5, TARSKI:def 1;
hence
[x,y] in the
InternalRel of
S
by ORDERS_2:def 9;
:: thesis: verum
end;
assume A6:
[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:106;
A7:
t1 <= t2
by A6, ORDERS_2:def 9;
t2 in {t2}
by TARSKI:def 1;
then
t1 in downarrow t2
by A7, WAYBEL_0:def 15;
then A8:
t1 in Cl {t2}
by WAYBEL11:9;
reconsider o1 =
x,
o2 =
y as
Element of
(Omega S) by A1, A6, ZFMISC_1:106;
o1 <= o2
by A8, Def2;
hence
[x,y] in the
InternalRel of
(Omega S)
by ORDERS_2:def 9;
:: thesis: verum
end;
hence
Omega S = TopRelStr(# the carrier of S,the InternalRel of S,the topology of S #)
by A1; :: thesis: verum