theorem :: WAYBEL15:32

for L being Boolean LATTICE holds
( 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 ) ) ) )