let L be Boolean LATTICE; :: thesis: ( L is arithmetic iff ex X being set st L, BoolePoset X are_isomorphic )

hereby :: thesis: ( ex X being set st L, BoolePoset X are_isomorphic implies L is arithmetic )

assume A1: L is arithmetic ; :: thesis: ex X being set st L, BoolePoset X are_isomorphic
then L opp is continuous by Th9, YELLOW_7:38;
then L is completely-distributive by A1, WAYBEL_6:39;
then for x being Element of L ex X being Subset of L st
( X c= ATOM L & x = sup X ) by Lm5;
hence ex X being set st L, BoolePoset X are_isomorphic by A1, Lm6; :: thesis: verum

end;

thus ( ex X being set st L, BoolePoset X are_isomorphic implies L is arithmetic ) by Th10, WAYBEL_1:6; :: thesis: verum