theorem :: WAYBEL29:33

for L being complete LATTICE holds
( InclPoset (sigma L) is continuous iff for S being complete LATTICE holds Sigma [:S,L:] = Omega [:(Sigma S),(Sigma L):] )