let L be complete LATTICE; :: thesis: ( ( for S being complete LATTICE holds sigma [:S,L:] = the topology of [:(Sigma S),(Sigma L):] ) iff for S being complete LATTICE holds TopStruct(# the carrier of (Sigma [:S,L:]), the topology of (Sigma [:S,L:]) #) = [:(Sigma S),(Sigma L):] )

let S be complete LATTICE; :: thesis: sigma [:S,L:] = the topology of [:(Sigma S),(Sigma L):]

TopStruct(# the carrier of (Sigma [:S,L:]), the topology of (Sigma [:S,L:]) #) = [:(Sigma S),(Sigma L):] by A3;

hence sigma [:S,L:] = the topology of [:(Sigma S),(Sigma L):] by YELLOW_9:51; :: thesis: verum

hereby :: thesis: ( ( for S being complete LATTICE holds TopStruct(# the carrier of (Sigma [:S,L:]), the topology of (Sigma [:S,L:]) #) = [:(Sigma S),(Sigma L):] ) implies for S being complete LATTICE holds sigma [:S,L:] = the topology of [:(Sigma S),(Sigma L):] )

assume A3:
for S being complete LATTICE holds TopStruct(# the carrier of (Sigma [:S,L:]), the topology of (Sigma [:S,L:]) #) = [:(Sigma S),(Sigma L):]
; :: thesis: for S being complete LATTICE holds sigma [:S,L:] = the topology of [:(Sigma S),(Sigma L):]assume A1:
for S being complete LATTICE holds sigma [:S,L:] = the topology of [:(Sigma S),(Sigma L):]
; :: thesis: for S being complete LATTICE holds TopStruct(# the carrier of (Sigma [:S,L:]), the topology of (Sigma [:S,L:]) #) = [:(Sigma S),(Sigma L):]

S_{8}[L]

end;S

proof

hence
for S being complete LATTICE holds TopStruct(# the carrier of (Sigma [:S,L:]), the topology of (Sigma [:S,L:]) #) = [:(Sigma S),(Sigma L):]
by Lm9; :: thesis: verum
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 (Sigma L), the InternalRel of (Sigma L) #) = RelStr(# the carrier of L, the InternalRel of L #) ) by YELLOW_9:def 4;

then A2: TopStruct(# the carrier of (Sigma L), the topology of (Sigma L) #) = 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 (Sigma S), the InternalRel of (Sigma S) #) = RelStr(# the carrier of S, the InternalRel of S #) ) by YELLOW_9:def 4;

then TopStruct(# the carrier of (Sigma S), the topology of (Sigma S) #) = TopStruct(# the carrier of SS, the topology of SS #) by Th13;

then [:SS,SL:] = [:(Sigma S),(Sigma L):] by A2, Th7;

hence sigma [:S,L:] = the topology of [:SS,SL:] by A1; :: thesis: verum

end;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 (Sigma L), the InternalRel of (Sigma L) #) = RelStr(# the carrier of L, the InternalRel of L #) ) by YELLOW_9:def 4;

then A2: TopStruct(# the carrier of (Sigma L), the topology of (Sigma L) #) = 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 (Sigma S), the InternalRel of (Sigma S) #) = RelStr(# the carrier of S, the InternalRel of S #) ) by YELLOW_9:def 4;

then TopStruct(# the carrier of (Sigma S), the topology of (Sigma S) #) = TopStruct(# the carrier of SS, the topology of SS #) by Th13;

then [:SS,SL:] = [:(Sigma S),(Sigma L):] by A2, Th7;

hence sigma [:S,L:] = the topology of [:SS,SL:] by A1; :: thesis: verum

let S be complete LATTICE; :: thesis: sigma [:S,L:] = the topology of [:(Sigma S),(Sigma L):]

TopStruct(# the carrier of (Sigma [:S,L:]), the topology of (Sigma [:S,L:]) #) = [:(Sigma S),(Sigma L):] by A3;

hence sigma [:S,L:] = the topology of [:(Sigma S),(Sigma L):] by YELLOW_9:51; :: thesis: verum