let A be Element of PL-WFF ; :: thesis: for F being Subset of PL-WFF holds F |- (('not' A) => A) => A
let F be Subset of PL-WFF; :: thesis: F |- (('not' A) => A) => A
(('not' A) => ('not' A)) => ((('not' A) => A) => A) in PL_axioms by withplax;
then A1: F |- (('not' A) => ('not' A)) => ((('not' A) => A) => A) by th42;
F |- ('not' A) => ('not' A) by thaa;
hence F |- (('not' A) => A) => A by A1, th43; :: thesis: verum