theorem Th50: :: SHEFFER2:50

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