theorem Th34: :: SHEFFER2:34

for L being non empty satisfying_Sh_1 ShefferStr
for x, y, z being Element of L holds x | (y | (x | (z | (y | x)))) = x | x