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

proof

let x be set ; :: 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 ext-real number holds
( e in X iff P₁[e] )
let e be ext-real number ; :: 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