let L be Boolean LATTICE; :: thesis: ( L is arithmetic iff ( L is continuous & L opp is continuous ) )

thus ( L is arithmetic implies ( L is continuous & L opp is continuous ) ) by Th9, YELLOW_7:38; :: thesis: ( L is continuous & L opp is continuous implies L is arithmetic )

assume that

A1: L is continuous and

A2: L opp is continuous ; :: thesis: L is arithmetic

L is completely-distributive by A1, A2, 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;

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

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

thus ( L is arithmetic implies ( L is continuous & L opp is continuous ) ) by Th9, YELLOW_7:38; :: thesis: ( L is continuous & L opp is continuous implies L is arithmetic )

assume that

A1: L is continuous and

A2: L opp is continuous ; :: thesis: L is arithmetic

L is completely-distributive by A1, A2, 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;

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

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