theorem :: HILBERT3:45

for a, b being Element of NAT st a <> b holds
not (((prop a) => (prop b)) => (prop a)) => (prop a) is pseudo-canonical