let A be complex-membered set ; :: thesis: for a being complex number holds
( a in A iff - a in -- A )
let a be complex number ; :: thesis: ( a in A iff - a in -- A )
a in COMPLEX by XCMPLX_0:def 2;
hence ( a in A implies - a in -- A ) ; :: thesis: ( - a in -- A implies a in A )
assume - a in -- A ; :: thesis: a in A
then ex c being Element of COMPLEX st
( - c = - a & c in A ) ;
hence a in A ; :: thesis: verum