theorem Th66: :: SHEFFER2:66

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