set X = { p where p is Element of PL-WFF : P1[p] } ;
{ p where p is Element of PL-WFF : P1[p] } c= PL-WFF
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { p where p is Element of PL-WFF : P1[p] } or x in PL-WFF )
assume x in { p where p is Element of PL-WFF : P1[p] } ; :: thesis: x in PL-WFF
then ex p being Element of PL-WFF st
( x = p & P1[p] ) ;
hence x in PL-WFF ; :: thesis: verum
end;
then reconsider X = { p where p is Element of PL-WFF : P1[p] } as Subset of PL-WFF ;
let r be Element of PL-WFF ; :: thesis: P1[r]
A4: X is with_propositional_variables
proof
let n be Element of NAT ; :: according to PL_AXIOM:def 1 :: thesis: <*(3 + n)*> in X
P1[ Prop n] by A2;
hence <*(3 + n)*> in X ; :: thesis: verum
end;
A5: X is with_implication
proof
let p be Element of PL-WFF ; :: according to PL_AXIOM:def 8 :: thesis: for q being Element of PL-WFF st p in X & q in X holds
p => q in X
let q be Element of PL-WFF ; :: thesis: ( p in X & q in X implies p => q in X )
assume p in X ; :: thesis: ( not q in X or p => q in X )
then A6: ex x being Element of PL-WFF st
( p = x & P1[x] ) ;
assume q in X ; :: thesis: p => q in X
then ex x being Element of PL-WFF st
( q = x & P1[x] ) ;
then P1[p => q] by A3, A6;
hence p => q in X ; :: thesis: verum
end;
PL-WFF c= NAT * by Def5;
then A8: X c= NAT * ;
X is with_FALSUM by A1;
then PL-WFF c= X by A8, A5, A4, Def6;
then r in X ;
then ex p being Element of PL-WFF st
( r = p & P1[p] ) ;
hence P1[r] ; :: thesis: verum