let A be Element of PL-WFF ; :: thesis: for F being Subset of PL-WFF st F is consistent & not F \/ {A} is consistent holds
F \/ {('not' A)} is consistent
let F be Subset of PL-WFF; :: thesis: ( F is consistent & not F \/ {A} is consistent implies F \/ {('not' A)} is consistent )
assume A1: ( F is consistent & not F \/ {A} is consistent ) ; :: 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;
then A6: F |- A by A2, th43;
F |- 'not' A by A1, conco, ded;
hence contradiction by A6, A1; :: thesis: verum