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 )

then for x being Element of L ex X being Subset of L st

( X c= ATOM L & x = sup X ) by Lm5;

then ex X being set st L, BoolePoset X are_isomorphic by A2, Lm6;

hence L is arithmetic by Th10, WAYBEL_1:6; :: thesis: verum

thus ( L is arithmetic implies L is completely-distributive ) :: thesis: ( L is completely-distributive implies L is arithmetic )

proof

assume A2:
L is completely-distributive
; :: thesis: L is arithmetic
assume A1:
L is arithmetic
; :: thesis: L is completely-distributive

then L opp is continuous by Th9, YELLOW_7:38;

hence L is completely-distributive by A1, WAYBEL_6:39; :: thesis: verum

end;then L opp is continuous by Th9, YELLOW_7:38;

hence L is completely-distributive by A1, WAYBEL_6:39; :: thesis: verum

then for x being Element of L ex X being Subset of L st

( X c= ATOM L & x = sup X ) by Lm5;

then ex X being set st L, BoolePoset X are_isomorphic by A2, Lm6;

hence L is arithmetic by Th10, WAYBEL_1:6; :: thesis: verum