theorem th3: :: PL_AXIOM:4

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