theorem naa: :: PL_AXIOM:61

for A being Element of PL-WFF
for F being Subset of PL-WFF holds F |- (('not' A) => A) => A