theorem :: SHEFFER1:26
for L being non empty Lattice-like Boolean well-complemented properly_defined ShefferOrthoLattStr holds L is satisfying_Sheffer_1