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

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

let x, y, z, p be Element of L; :: thesis: y = (((x | x) | x) | y) | ((z | z) | y)
(y | (((p | (p | p)) | (p | (p | p))) | z)) | (y | (((p | (p | p)) | (p | (p | p))) | z)) = y by Th124;
hence y = (((x | x) | x) | y) | ((z | z) | y) by Th110; :: thesis: verum

end;

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