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

proof

let x be object ; :: according to MEMBERED:def 4 :: thesis: ( x in X implies x is rational )
assume x in X ; :: thesis: x is rational
then x in RAT by A1;
hence x is rational ; :: thesis: verum

end;

then reconsider X = X as rational-membered set ;
take X ; :: thesis: for w being Rational holds
( w in X iff P₁[w] )
let w be Rational; :: thesis: ( w in X iff P₁[w] )
w in RAT by RAT_1:def 2;
hence ( w in X iff P₁[w] ) by A1; :: thesis: verum