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