theorem Th32: :: SHEFFER1:32

for L being non empty properly_defined satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferOrthoLattStr
for x, y being Element of L holds x | (x | x) = y | (y | y)