let L be complete LATTICE; :: thesis: ( InclPoset (sigma L) is continuous iff for S being complete LATTICE holds Sigma [:S,L:] = Omega [:(Sigma S),(Sigma L):] )
( InclPoset (sigma L) is continuous iff for S being complete LATTICE holds sigma [:S,L:] = the topology of [:(Sigma S),(Sigma L):] ) by Th30;
hence ( InclPoset (sigma L) is continuous iff for S being complete LATTICE holds Sigma [:S,L:] = Omega [:(Sigma S),(Sigma L):] ) by Th32; :: thesis: verum