let L be complete LATTICE; :: thesis: ( ( for S being complete LATTICE holds sigma [:S,L:] = the topology of [:(),():] ) iff for S being complete LATTICE holds TopStruct(# the carrier of (Sigma [:S,L:]), the topology of (Sigma [:S,L:]) #) = [:(),():] )
hereby :: thesis: ( ( for S being complete LATTICE holds TopStruct(# the carrier of (Sigma [:S,L:]), the topology of (Sigma [:S,L:]) #) = [:(),():] ) implies for S being complete LATTICE holds sigma [:S,L:] = the topology of [:(),():] )
assume A1: for S being complete LATTICE holds sigma [:S,L:] = the topology of [:(),():] ; :: thesis: for S being complete LATTICE holds TopStruct(# the carrier of (Sigma [:S,L:]), the topology of (Sigma [:S,L:]) #) = [:(),():]
S8[L]
proof
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:]
( RelStr(# the carrier of SL, the InternalRel of SL #) = RelStr(# the carrier of L, the InternalRel of L #) & RelStr(# the carrier of (), the InternalRel of () #) = RelStr(# the carrier of L, the InternalRel of L #) ) by YELLOW_9:def 4;
then A2: TopStruct(# the carrier of (), the topology of () #) = TopStruct(# the carrier of SL, the topology of SL #) by Th13;
( RelStr(# the carrier of SS, the InternalRel of SS #) = RelStr(# the carrier of S, the InternalRel of S #) & RelStr(# the carrier of (), the InternalRel of () #) = RelStr(# the carrier of S, the InternalRel of S #) ) by YELLOW_9:def 4;
then TopStruct(# the carrier of (), the topology of () #) = TopStruct(# the carrier of SS, the topology of SS #) by Th13;
then [:SS,SL:] = [:(),():] by ;
hence sigma [:S,L:] = the topology of [:SS,SL:] by A1; :: thesis: verum
end;
hence for S being complete LATTICE holds TopStruct(# the carrier of (Sigma [:S,L:]), the topology of (Sigma [:S,L:]) #) = [:(),():] by Lm9; :: thesis: verum
end;
assume A3: for S being complete LATTICE holds TopStruct(# the carrier of (Sigma [:S,L:]), the topology of (Sigma [:S,L:]) #) = [:(),():] ; :: thesis: for S being complete LATTICE holds sigma [:S,L:] = the topology of [:(),():]
let S be complete LATTICE; :: thesis: sigma [:S,L:] = the topology of [:(),():]
TopStruct(# the carrier of (Sigma [:S,L:]), the topology of (Sigma [:S,L:]) #) = [:(),():] by A3;
hence sigma [:S,L:] = the topology of [:(),():] by YELLOW_9:51; :: thesis: verum