let L be Boolean LATTICE; :: thesis: ( L is arithmetic iff L is continuous )
thus ( L is arithmetic implies L is continuous ) ; :: thesis: ( L is continuous implies L is arithmetic )
assume A1: L is continuous ; :: thesis: L is arithmetic
then L opp is continuous by Th11, 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 Lm4;
then ex X being set st L, BoolePoset X are_isomorphic by A1, Lm5;
hence L is arithmetic by Th12, WAYBEL_1:7; :: thesis: verum