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 S1[ Element of PL-WFF ] means $1 in HP-WFF ;
VERUM = FaLSUM ;
then A1: S1[ FaLSUM ] ;
A2: for n being Element of NAT holds S1[ Prop n]
proof
let n be Element of NAT ; :: thesis: S1[ Prop n]
Prop n = prop n ;
hence S1[ Prop n] ; :: thesis: verum
end;
A3: for r, s being Element of PL-WFF st S1[r] & S1[s] holds
S1[r => s]
proof
let r, s be Element of PL-WFF ; :: thesis: ( S1[r] & S1[s] implies S1[r => s] )
assume ( S1[r] & S1[s] ) ; :: thesis: S1[r => s]
then reconsider r1 = r, s1 = s as Element of HP-WFF ;
r1 => s1 in HP-WFF ;
hence S1[r => s] ; :: thesis: verum
end;
A4: for A being Element of PL-WFF holds S1[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