theorem :: WAYBEL_6:38

for L being complete LATTICE holds
( L is completely-distributive iff ( L is continuous & ( for l being Element of L ex X being Subset of L st
( l = sup X & ( for x being Element of L st x in X holds
x is co-prime ) ) ) ) )