theorem th2: :: PL_AXIOM:3

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