theorem Th8: :: SHEFFER1:8

for L being non empty join-commutative meet-commutative distributive upper-bounded' lower-bounded' distributive' complemented' LattStr holds L is meet-idempotent