let L be complete LATTICE; :: thesis: ( 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 ) ) ) ) )
thus ( L is completely-distributive implies ( 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 ) ) ) ) ) :: thesis: ( 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 ) ) ) implies L is completely-distributive )

proof

assume L is completely-distributive ; :: thesis: ( 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 ) ) ) )
then reconsider L = L as completely-distributive LATTICE ;
L ~ is continuous by Lm3;
hence ( 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 ) ) ) ) by Lm4; :: thesis: verum

end;

thus ( 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 ) ) ) implies L is completely-distributive ) by Lm2; :: thesis: verum