let L be Boolean LATTICE; :: thesis: ( L is arithmetic iff L is completely-distributive )
thus ( L is arithmetic implies L is completely-distributive ) :: thesis: ( L is completely-distributive implies L is arithmetic )

proof

assume L is arithmetic ; :: thesis: L is completely-distributive
then ( L is continuous & L opp is continuous ) by Th11, YELLOW_7:38;
hence L is completely-distributive by WAYBEL_6:39; :: thesis: verum

end;

assume L is completely-distributive ; :: thesis: L is arithmetic
then ( L is complete & ( for x being Element of L ex X being Subset of L st
( X c= ATOM L & x = sup X ) ) ) by Lm6;
then ex X being set st L, BoolePoset X are_isomorphic by Lm7;
hence L is arithmetic by Th12, WAYBEL_1:7; :: thesis: verum