theorem Th62: :: SHEFFER2:62

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