let L be non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr ; :: thesis: for z, y being Element of L holds (y | ((y | y) | z)) | (y | ((y | y) | z)) = y

now :: thesis: for z, y, x being Element of L holds (y | ((y | y) | z)) | (y | ((y | y) | z)) = y

let z, y, x be Element of L; :: thesis: (y | ((y | y) | z)) | (y | ((y | y) | z)) = y
(((x | x) | x) | y) | ((z | z) | y) = y by Th127;
hence (y | ((y | y) | z)) | (y | ((y | y) | z)) = y by Th114; :: thesis: verum

end;

hence for z, y being Element of L holds (y | ((y | y) | z)) | (y | ((y | y) | z)) = y ; :: thesis: verum