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)

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

hence z | (x | p) = z | (p | x) by Th151; :: thesis: verum