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

proof

let x be object ; :: according to MEMBERED:def 3 :: thesis: ( x in X implies x is real )
assume x in X ; :: thesis: x is real
then x in REAL by A1;
hence x is real ; :: thesis: verum

end;

then reconsider X = X as real-membered set ;
take X ; :: thesis: for r being Real holds
( r in X iff P₁[r] )
let r be Real; :: thesis: ( r in X iff P₁[r] )
r in REAL by XREAL_0:def 1;
hence ( r in X iff P₁[r] ) by A1; :: thesis: verum