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

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

let q, p, x be Element of L; :: thesis: p | (x | p) = (x | x) | p
((p | (x | p)) | (p | (x | p))) | (q | (q | q)) = p | (x | p) by Th71;
hence p | (x | p) = (x | x) | p by Th118; :: thesis: verum

end;

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