theorem Th31: :: WAYBEL29:31

for L being complete LATTICE holds
( ( 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):] )