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

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

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

end;

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