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

proof

let x be object ; :: according to MEMBERED:def 6 :: thesis: ( x in X implies x is natural )
assume x in X ; :: thesis: x is natural
then x in NAT by A1;
hence x is natural ; :: thesis: verum

end;

then reconsider X = X as natural-membered set ;
take X ; :: thesis: for n being Nat holds
( n in X iff P₁[n] )
let n be Nat; :: thesis: ( n in X iff P₁[n] )
n in NAT by ORDINAL1:def 12;
hence ( n in X iff P₁[n] ) by A1; :: thesis: verum