let x be Real; :: thesis: for x1 being Point of RNS_Real st x = x1 holds
- x = - x1
let x1 be Point of RNS_Real; :: thesis: ( x = x1 implies - x = - x1 )
assume AS: x = x1 ; :: thesis: - x = - x1
reconsider mx = - x as Point of RNS_Real by XREAL_0:def 1;
x1 + mx = x + (- x) by AS, BINOP_2:def 9;
then x1 + mx = 0. RNS_Real ;
hence - x = - x1 by RLVECT_1:def 10; :: thesis: verum