let L be complete LATTICE; :: thesis: ( L is completely-distributive iff ( L is distributive & L is continuous & L opp is continuous ) )
thus ( L is completely-distributive implies ( L is distributive & L is continuous & L ~ is continuous ) ) by Lm3; :: thesis: ( L is distributive & L is continuous & L opp is continuous implies L is completely-distributive )
assume that
A1: ( L is distributive & L is continuous ) and
A2: L ~ is continuous ; :: thesis: L is completely-distributive
reconsider L = L as distributive continuous LATTICE by A1;
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 A2, Lm4;
hence L is completely-distributive by Lm2; :: thesis: verum