theorem Th17: :: PL_AXIOM:30

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