theorem Th17a: :: PL_AXIOM:13

for p, q being boolean object holds (('not' q) => ('not' p)) => ((('not' q) => p) => q) = TRUE