set X = { p where p is Element of HP-WFF : P₁[p] } ;
{ p where p is Element of HP-WFF : P₁[p] } c= HP-WFF

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

end;

then reconsider X = { p where p is Element of HP-WFF : P₁[p] } as Subset of HP-WFF ;
let r be Element of HP-WFF ; :: thesis:
A4: X is with_propositional_variables

let n be Element of NAT ; :: according to HILBERT2:def 3 :: thesis:
P₁[ prop n] by A2;
hence prop n in X ; :: thesis:

end;

A5: X is with_implication

let p be Element of HP-WFF ; :: according to HILBERT2:def 4 :: thesis:
let q be Element of HP-WFF ; :: thesis:
assume p in X ; :: thesis:
then A6: ex x being Element of HP-WFF st
( p = x & P₁[x] ) ;
assume q in X ; :: thesis:
then ex x being Element of HP-WFF st
( q = x & P₁[x] ) ;
then P₁[p => q] by A3, A6;
hence p => q in X ; :: thesis:

end;

A7: HP-WFF c= NAT * by HILBERT1:def 5;
A8: X c= NAT * by A7;
A9: X is with_conjunction

let p be Element of HP-WFF ; :: according to HILBERT2:def 5 :: thesis:
let q be Element of HP-WFF ; :: thesis:
assume p in X ; :: thesis:
then A10: ex x being Element of HP-WFF st
( p = x & P₁[x] ) ;
assume q in X ; :: thesis:
then ex x being Element of HP-WFF st
( q = x & P₁[x] ) ;
then P₁[p '&' q] by A3, A10;
hence p '&' q in X ; :: thesis:

end;

VERUM in X by A1;
then X is with_VERUM ;
then HP-WFF c= X by A8, A5, A9, A4, HILBERT1:def 6;
then r in X ;
then ex p being Element of HP-WFF st
( r = p & P₁[p] ) ;
hence P₁[r] ; :: thesis: