let A be Subset of REAL; :: thesis: for x being Real st x in -- A holds
ex a being Real st
( a in A & x = - a )
let x be Real; :: thesis: ( x in -- A implies ex a being Real st
( a in A & x = - a ) )
assume x in -- A ; :: thesis: ex a being Real st
( a in A & x = - a )
then x in { (- a) where a is Complex : a in A } ;
then consider a being Complex such that
A1: ( x = - a & a in A ) ;
reconsider a = a as Real by A1;
take a ; :: thesis: ( a in A & x = - a )
thus ( a in A & x = - a ) by A1; :: thesis: verum