theorem th34: :: PL_AXIOM:63

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