defpred S₁[ set ] means ex x being R_eal st
( x = $1 & P₁[x] );
consider X being set such that
A1: for r being set holds
( r in X iff ( r in REAL \/ {-infty ,+infty } & S₁[r] ) ) from XBOOLE_0:sch 1();
X c= REAL \/ {-infty ,+infty }

proof

let r be set ; :: according to TARSKI:def 3 :: thesis: ( not r in X or r in REAL \/ {-infty ,+infty } )
assume r in X ; :: thesis: r in REAL \/ {-infty ,+infty }
hence r in REAL \/ {-infty ,+infty } by A1; :: thesis: verum

end;

then reconsider X = X as Subset of ExtREAL ;
take X ; :: thesis: for x being R_eal holds
( x in X iff P₁[x] )
let x be R_eal; :: thesis: ( x in X iff P₁[x] )

hereby :: thesis: ( P₁[x] implies x in X )

assume x in X ; :: thesis: P₁[x]
then ex y being R_eal st
( y = x & P₁[y] ) by A1;
hence P₁[x] ; :: thesis: verum

end;

assume P₁[x] ; :: thesis: x in X
hence x in X by A1; :: thesis: verum