let L be Boolean LATTICE; :: thesis: ( L is arithmetic iff ( L is complete & ( for x being Element of L ex X being Subset of L st

( X c= ATOM L & x = sup X ) ) ) )

( X c= ATOM L & x = sup X ) ) ) ; :: thesis: L is arithmetic

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

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

( X c= ATOM L & x = sup X ) ) ) )

hereby :: thesis: ( L is complete & ( for x being Element of L ex X being Subset of L st

( X c= ATOM L & x = sup X ) ) implies L is arithmetic )

assume
( L is complete & ( for x being Element of L ex X being Subset of L st ( X c= ATOM L & x = sup X ) ) implies L is arithmetic )

assume A1:
L is arithmetic
; :: thesis: ( L is complete & ( for x being Element of L ex X being Subset of L st

( X c= ATOM L & x = sup X ) ) )

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

then L is completely-distributive by A1, WAYBEL_6:39;

hence ( L is complete & ( for x being Element of L ex X being Subset of L st

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

end;( X c= ATOM L & x = sup X ) ) )

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

then L is completely-distributive by A1, WAYBEL_6:39;

hence ( L is complete & ( for x being Element of L ex X being Subset of L st

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

( X c= ATOM L & x = sup X ) ) ) ; :: thesis: L is arithmetic

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

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