theorem Th25: :: SHEFFER1:25

for L being non empty LattStr holds
( L is Boolean Lattice iff ( L is lower-bounded' & L is upper-bounded' & L is join-commutative & L is meet-commutative & L is distributive & L is distributive' & L is complemented' ) )