consider X being set such that
A1: for x being object holds
( x in X iff ( x in INT & P₁[x] ) ) from XBOOLE_0:sch 1();
X is integer-membered

proof

let x be object ; :: according to MEMBERED:def 5 :: thesis: ( x in X implies x is integer )
assume x in X ; :: thesis: x is integer
then x in INT by A1;
hence x is integer ; :: thesis: verum

end;

then reconsider X = X as integer-membered set ;
take X ; :: thesis: for i being Integer holds
( i in X iff P₁[i] )
let i be Integer; :: thesis: ( i in X iff P₁[i] )
i in INT by INT_1:def 2;
hence ( i in X iff P₁[i] ) by A1; :: thesis: verum