theorem :: PL_AXIOM:42

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