let A be Element of PL-WFF ; :: thesis: for F being Subset of PL-WFF st not F |- A holds
F \/ {('not' A)} is consistent
let F be Subset of PL-WFF; :: thesis: ( not F |- A implies F \/ {('not' A)} is consistent )
assume Z1: not F |- A ; :: thesis: F \/ {('not' A)} is consistent
assume not F \/ {('not' A)} is consistent ; :: thesis: contradiction
then A2: F |- ('not' A) => A by ded, conco;
F |- (('not' A) => A) => A by naa;
hence contradiction by Z1, A2, th43; :: thesis: verum