let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in PL-WFF or x in HP-WFF )
assume A0: x in PL-WFF ; :: thesis: x in HP-WFF
defpred S₁[ Element of PL-WFF ] means $1 in HP-WFF ;
VERUM = FaLSUM ;
then A1: S₁[ FaLSUM ] ;
A2: for n being Element of NAT holds S₁[ Prop n]

proof

let n be Element of NAT ; :: thesis: S₁[ Prop n]
Prop n = prop n ;
hence S₁[ Prop n] ; :: thesis: verum

end;

A3: for r, s being Element of PL-WFF st S₁[r] & S₁[s] holds
S₁[r => s]

proof

let r, s be Element of PL-WFF ; :: thesis: ( S₁[r] & S₁[s] implies S₁[r => s] )
assume ( S₁[r] & S₁[s] ) ; :: thesis: S₁[r => s]
then reconsider r1 = r, s1 = s as Element of HP-WFF ;
r1 => s1 in HP-WFF ;
hence S₁[r => s] ; :: thesis: verum

end;

A4: for A being Element of PL-WFF holds S₁[A] from PL_AXIOM:sch 1(A1, A2, A3);
reconsider x1 = x as Element of PL-WFF by A0;
x1 in HP-WFF by A4;
hence x in HP-WFF ; :: thesis: verum