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

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

let x, w, p, z be Element of L; :: thesis: w | (z | ((x | x) | w)) = w | (x | z)
(((x | x) | w) | ((z | (p | (p | p))) | w)) | w = w | (z | ((x | x) | w)) by Th143;
hence w | (z | ((x | x) | w)) = w | (x | z) by Th147; :: thesis: verum

end;

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