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