let A be complex-membered set ; :: thesis: for a being Complex holds
( a in A iff - a in -- A )
let a be Complex; :: thesis: ( a in A iff - a in -- A )
thus ( 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 Complex st
( - c = - a & c in A ) ;
hence a in A ; :: thesis: verum