theorem :: PL_AXIOM:44

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