let L be complete LATTICE; :: thesis: ( S8[L] iff S9[L] )
thus ( S8[L] implies S9[L] ) :: thesis: ( S9[L] implies S8[L] )
proof
assume A1: S8[L] ; :: thesis: S9[L]
let SL be Scott TopAugmentation of L; :: thesis: 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; :: thesis: 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; :: thesis: 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:]; :: thesis: 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
.= the carrier of [:SS,SL:] by BORSUK_1:def 2 ;
hence TopStruct(# the carrier of SSL, the topology of SSL #) = [:SS,SL:] by A2; :: thesis: verum
end;
assume A4: S9[L] ; :: thesis: S8[L]
let SL be Scott TopAugmentation of L; :: thesis: 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; :: thesis: for SS being Scott TopAugmentation of S holds sigma [:S,L:] = the topology of [:SS,SL:]
let SS be Scott TopAugmentation of S; :: thesis: sigma [:S,L:] = the topology of [:SS,SL:]
now :: thesis: for SSL being Scott TopAugmentation of [:S,L:] holds sigma [:S,L:] = the topology of [:SS,SL:]
let SSL be Scott TopAugmentation of [:S,L:]; :: thesis: sigma [:S,L:] = the topology of [:SS,SL:]
TopStruct(# the carrier of SSL, the topology of SSL #) = TopStruct(# the carrier of [:SS,SL:], the topology of [:SS,SL:] #) by A4;
hence sigma [:S,L:] = the topology of [:SS,SL:] by YELLOW_9:51; :: thesis: verum
end;
hence sigma [:S,L:] = the topology of [:SS,SL:] ; :: thesis: verum