let z be Complex; :: thesis: ( Re (- z) = - (Re z) & Im (- z) = - (Im z) )
- z = (- (Re z)) + ((- (Im z)) * <i>) by Lm22;
hence ( Re (- z) = - (Re z) & Im (- z) = - (Im z) ) by Th12; :: thesis: verum