defpred S₁[ set ] means ex i0 being Integer st
( i0 = $1 & P₁[i0] );
consider X being set such that
A1: for y being set holds
( y in X iff ( y in INT & S₁[y] ) ) from XBOOLE_0:sch 1();
for y being set st y in X holds
y in INT by A1;
then reconsider X = X as Subset of INT by TARSKI:def 3;
take X ; :: thesis: for x being Integer holds
( x in X iff P₁[x] )
let i0 be Integer; :: thesis: ( i0 in X iff P₁[i0] )
A2: ( i0 in X implies P₁[i0] )

proof

assume i0 in X ; :: thesis: P₁[i0]
then ex i1 being Integer st
( i0 = i1 & P₁[i1] ) by A1;
hence P₁[i0] ; :: thesis: verum

end;

( P₁[i0] implies i0 in X )

proof

assume A3: P₁[i0] ; :: thesis: i0 in X
i0 in INT by Def2;
hence i0 in X by A1, A3; :: thesis: verum

end;

hence ( i0 in X iff P₁[i0] ) by A2; :: thesis: verum