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 Sigma [:S,L:] = Omega [:(),():] )
hereby :: thesis: ( ( for S being complete LATTICE holds Sigma [:S,L:] = Omega [:(),():] ) 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 Sigma [:S,L:] = Omega [:(),():]
let S be complete LATTICE; :: thesis: Sigma [:S,L:] = Omega [:(),():]
TopStruct(# the carrier of (Sigma [:S,L:]), the topology of (Sigma [:S,L:]) #) = [:(),():] by ;
then Omega (Sigma [:S,L:]) = Omega [:(),():] by WAYBEL25:13;
hence Sigma [:S,L:] = Omega [:(),():] by WAYBEL25:15; :: thesis: verum
end;
assume A2: for S being complete LATTICE holds Sigma [:S,L:] = Omega [:(),():] ; :: 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 [:(),():]
Sigma [:S,L:] = Omega [:(),():] by A2;
then TopStruct(# the carrier of (Sigma [:S,L:]), the topology of (Sigma [:S,L:]) #) = [:(),():] by WAYBEL25:def 2;
hence sigma [:S,L:] = the topology of [:(),():] by YELLOW_9:51; :: thesis: verum