let F be Subset of PL-WFF; :: thesis: ( F is consistent iff not for A being Element of PL-WFF holds F |- A )
hereby :: thesis: ( not for A being Element of PL-WFF holds F |- A implies F is consistent )
assume A0: F is consistent ; :: thesis: not for A being Element of PL-WFF holds F |- A
assume A1: for A being Element of PL-WFF holds F |- A ; :: thesis: contradiction
then A2: F |- Prop 0 ;
F |- 'not' (Prop 0) by A1;
hence contradiction by A2, A0; :: thesis: verum
end;
assume A4: not for A being Element of PL-WFF holds F |- A ; :: thesis: F is consistent
assume not F is consistent ; :: thesis: contradiction
then consider A being Element of PL-WFF such that
A3: ( F |- A & F |- 'not' A ) ;
now :: thesis: for B being Element of PL-WFF holds F |- B
let B be Element of PL-WFF ; :: thesis: F |- B
F |- ('not' A) => (A => B) by naab;
then F |- A => B by A3, th43;
hence F |- B by A3, th43; :: thesis: verum
end;
hence contradiction by A4; :: thesis: verum