defpred S₁[ set ] means for T being Subset of HP-WFF st T is Hilbert_theory & X c= T holds
$1 in T;
consider Y being set such that
A1: for a being set holds
( a in Y iff ( a in HP-WFF & S₁[a] ) ) from XBOOLE_0:sch 1();
Y c= HP-WFF

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in Y or a in HP-WFF )
assume a in Y ; :: thesis: a in HP-WFF
hence a in HP-WFF by A1; :: thesis: verum

end;

then reconsider Z = Y as Subset of HP-WFF ;
take Z ; :: thesis: for r being Element of HP-WFF holds
( r in Z iff for T being Subset of HP-WFF st T is Hilbert_theory & X c= T holds
r in T )
thus for r being Element of HP-WFF holds
( r in Z iff for T being Subset of HP-WFF st T is Hilbert_theory & X c= T holds
r in T ) by A1; :: thesis: verum