theorem onecon: :: PL_AXIOM:67

for A being Element of PL-WFF
for F being Subset of PL-WFF st F is consistent & not F \/ {A} is consistent holds
F \/ {('not' A)} is consistent