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 Sigma [:S,L:] = Omega [:(Sigma S),(Sigma L):] )

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

Sigma [:S,L:] = Omega [:(Sigma S),(Sigma L):] by A2;

then TopStruct(# the carrier of (Sigma [:S,L:]), the topology of (Sigma [:S,L:]) #) = [:(Sigma S),(Sigma L):] by WAYBEL25:def 2;

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 Sigma [:S,L:] = Omega [:(Sigma S),(Sigma L):] ) implies for S being complete LATTICE holds sigma [:S,L:] = the topology of [:(Sigma S),(Sigma L):] )

assume A2:
for S being complete LATTICE holds Sigma [:S,L:] = Omega [:(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 Sigma [:S,L:] = Omega [:(Sigma S),(Sigma L):]

let S be complete LATTICE; :: thesis: Sigma [:S,L:] = Omega [:(Sigma S),(Sigma L):]

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

then Omega (Sigma [:S,L:]) = Omega [:(Sigma S),(Sigma L):] by WAYBEL25:13;

hence Sigma [:S,L:] = Omega [:(Sigma S),(Sigma L):] by WAYBEL25:15; :: thesis: verum

end;let S be complete LATTICE; :: thesis: Sigma [:S,L:] = Omega [:(Sigma S),(Sigma L):]

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

then Omega (Sigma [:S,L:]) = Omega [:(Sigma S),(Sigma L):] by WAYBEL25:13;

hence Sigma [:S,L:] = Omega [:(Sigma S),(Sigma L):] by WAYBEL25:15; :: thesis: verum

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

Sigma [:S,L:] = Omega [:(Sigma S),(Sigma L):] by A2;

then TopStruct(# the carrier of (Sigma [:S,L:]), the topology of (Sigma [:S,L:]) #) = [:(Sigma S),(Sigma L):] by WAYBEL25:def 2;

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