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

proof

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

end;

then reconsider X = X as ext-real-membered set ;
take X ; :: thesis: for e being ExtReal holds
( e in X iff P₁[e] )
let e be ExtReal; :: thesis: ( e in X iff P₁[e] )
e in ExtREAL by XXREAL_0:def 1;
hence ( e in X iff P₁[e] ) by A1; :: thesis: verum