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 )

( 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

( 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

thus
( L is continuous & ( for l being Element of L ex X being Subset of L st
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;( 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

( 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