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

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