defpred S₁[ Element of PL_axioms ] means ( $1 is axpl1 or $1 is axpl2 or $1 is axpl3 );
set X = { p where p is Element of PL_axioms : S₁[p] } ;
{ p where p is Element of PL_axioms : S₁[p] } c= PL-WFF

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in { p where p is Element of PL_axioms : S₁[p] } ; :: thesis:
then ex p being Element of PL_axioms st
( x = p & S₁[p] ) ;
hence x in PL-WFF ; :: thesis:

end;

then reconsider X = { p where p is Element of PL_axioms : S₁[p] } as Subset of PL-WFF ;
let A be Element of PL_axioms ; :: thesis:
X is with_PL_axioms

let p be Element of PL-WFF ; :: according to PL_AXIOM:def 19 :: thesis:
let q, r be Element of PL-WFF ; :: thesis:
thus p => (q => p) in X :: thesis:

reconsider pp = p => (q => p) as Element of PL_axioms by withplax;
S₁[pp] by defaxpl1;
hence p => (q => p) in X ; :: thesis:

end;

thus (p => (q => r)) => ((p => q) => (p => r)) in X :: thesis:

reconsider pp = (p => (q => r)) => ((p => q) => (p => r)) as Element of PL_axioms by withplax;
S₁[pp] by defaxpl2;
hence (p => (q => r)) => ((p => q) => (p => r)) in X ; :: thesis:

end;

reconsider pp = (('not' q) => ('not' p)) => ((('not' q) => p) => q) as Element of PL_axioms by withplax;
S₁[pp] by defaxpl3;
hence (('not' q) => ('not' p)) => ((('not' q) => p) => q) in X ; :: thesis:

end;