theorem Th36: :: SHEFFER1:36

for L being non empty properly_defined satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferOrthoLattStr holds L is distributive'