theorem th4: :: PL_AXIOM:6

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