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