defpred S₁[ R_eal] means ex x being R_eal st
( x in X & $1 = - x );
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();
consider x being Element of X;
- x = - x ;
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 being R_eal st
( x in X & z = - x ) )
thus for z being R_eal holds
( z in Z iff ex x being R_eal st
( x in X & z = - x ) ) by A1; :: thesis: verum