let L be complete LATTICE; ( S8[L] iff S9[L] )
thus
( S8[L] implies S9[L] )
( S9[L] implies S8[L] )proof
assume A1:
S8[
L]
;
S9[L]
let SL be
Scott TopAugmentation of
L;
for S being complete LATTICE
for SS being Scott TopAugmentation of S
for SSL being Scott TopAugmentation of [:S,L:] holds TopStruct(# the carrier of SSL, the topology of SSL #) = [:SS,SL:]let S be
complete LATTICE;
for SS being Scott TopAugmentation of S
for SSL being Scott TopAugmentation of [:S,L:] holds TopStruct(# the carrier of SSL, the topology of SSL #) = [:SS,SL:]let SS be
Scott TopAugmentation of
S;
for SSL being Scott TopAugmentation of [:S,L:] holds TopStruct(# the carrier of SSL, the topology of SSL #) = [:SS,SL:]let SSL be
Scott TopAugmentation of
[:S,L:];
TopStruct(# the carrier of SSL, the topology of SSL #) = [:SS,SL:]
A2: the
topology of
[:SS,SL:] =
sigma [:S,L:]
by A1
.=
the
topology of
SSL
by YELLOW_9:51
;
A3:
RelStr(# the
carrier of
SSL, the
InternalRel of
SSL #)
= RelStr(# the
carrier of
[:S,L:], the
InternalRel of
[:S,L:] #)
by YELLOW_9:def 4;
(
RelStr(# the
carrier of
SL, the
InternalRel of
SL #)
= RelStr(# the
carrier of
L, the
InternalRel of
L #) &
RelStr(# the
carrier of
SS, the
InternalRel of
SS #)
= RelStr(# the
carrier of
S, the
InternalRel of
S #) )
by YELLOW_9:def 4;
then the
carrier of
SSL =
[: the carrier of SS, the carrier of SL:]
by A3, YELLOW_3:def 2
.=
the
carrier of
[:SS,SL:]
by BORSUK_1:def 2
;
hence
TopStruct(# the
carrier of
SSL, the
topology of
SSL #)
= [:SS,SL:]
by A2;
verum
end;
assume A4:
S9[L]
; S8[L]
let SL be Scott TopAugmentation of L; for S being complete LATTICE
for SS being Scott TopAugmentation of S holds sigma [:S,L:] = the topology of [:SS,SL:]
let S be complete LATTICE; for SS being Scott TopAugmentation of S holds sigma [:S,L:] = the topology of [:SS,SL:]
let SS be Scott TopAugmentation of S; sigma [:S,L:] = the topology of [:SS,SL:]
hence
sigma [:S,L:] = the topology of [:SS,SL:]
; verum