let A, B be Element of PL-WFF ; :: thesis: for F being Subset of PL-WFF holds F |- ('not' A) => (A => B)
let F be Subset of PL-WFF; :: thesis: F |- ('not' A) => (A => B)
set f = (F \/ {('not' A)}) \/ {A};
A in (F \/ {('not' A)}) \/ {A} by ZFMISC_1:31, XBOOLE_1:11;
then A1: (F \/ {('not' A)}) \/ {A} |- A by th42;
(F \/ {('not' A)}) \/ {A} = (F \/ {A}) \/ {('not' A)} by XBOOLE_1:4;
then 'not' A in (F \/ {('not' A)}) \/ {A} by ZFMISC_1:31, XBOOLE_1:11;
then A2: (F \/ {('not' A)}) \/ {A} |- 'not' A by th42;
A => (('not' B) => A) in PL_axioms by withplax;
then (F \/ {('not' A)}) \/ {A} |- A => (('not' B) => A) by th42;
then A4: (F \/ {('not' A)}) \/ {A} |- ('not' B) => A by th43, A1;
('not' A) => (('not' B) => ('not' A)) in PL_axioms by withplax;
then (F \/ {('not' A)}) \/ {A} |- ('not' A) => (('not' B) => ('not' A)) by th42;
then A3: (F \/ {('not' A)}) \/ {A} |- ('not' B) => ('not' A) by th43, A2;
(('not' B) => ('not' A)) => ((('not' B) => A) => B) in PL_axioms by withplax;
then (F \/ {('not' A)}) \/ {A} |- (('not' B) => ('not' A)) => ((('not' B) => A) => B) by th42;
then (F \/ {('not' A)}) \/ {A} |- (('not' B) => A) => B by th43, A3;
then (F \/ {('not' A)}) \/ {A} |- B by th43, A4;
then F \/ {('not' A)} |- A => B by ded;
hence F |- ('not' A) => (A => B) by ded; :: thesis: verum