theorem Th33: :: SHEFFER1:33

for L being non empty properly_defined satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferOrthoLattStr holds L is join-commutative