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):] )

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

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):]
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