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

hence
for p, x being Element of L holds p | (x | p) = (x | x) | p
; :: thesis: verumlet 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;((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