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 )
- (- a) = a ;
hence ( - a in A iff a in -- A ) by Th11; :: thesis: verum