theorem :: PL_AXIOM:31

for p, q being Element of PL-WFF holds (p => q) => (('not' q) => ('not' p)) is tautology