theorem Th128: :: SHEFFER2:128

for L being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for z, y being Element of L holds (y | ((y | y) | z)) | (y | ((y | y) | z)) = y