theorem th3a: :: PL_AXIOM:5

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