:: deftheorem Def1 defines BooleLatt LATTICE3:def 1 :
for X being set
for b₂ being strict LattStr holds
( b₂ = BooleLatt X iff ( the carrier of b₂ = bool X & ( for Y, Z being Subset of X holds
( the L_join of b₂ . (Y,Z) = Y \/ Z & the L_meet of b₂ . (Y,Z) = Y /\ Z ) ) ) );