consider y being Element of Y;
consider x being Element of X;
defpred S₁[ R_eal] means ex x, y being R_eal st
( x in X & y in Y & $1 = x + y );
consider Z being Subset of ExtREAL such that
A1: for z being R_eal holds
( z in Z iff S₁[z] ) from SUBSET_1:sch 3();
x + y = x + y ;
then reconsider Z = Z as non empty Subset of ExtREAL by A1;
take Z ; :: thesis: for z being R_eal holds
( z in Z iff ex x, y being R_eal st
( x in X & y in Y & z = x + y ) )
thus for z being R_eal holds
( z in Z iff ex x, y being R_eal st
( x in X & y in Y & z = x + y ) ) by A1; :: thesis: verum