let n be Nat; :: thesis: for x being Element of REAL n holds
( x - x = 0* n & x + (- x) = 0* n )
let x be Element of REAL n; :: thesis: ( x - x = 0* n & x + (- x) = 0* n )
thus x - x = 0* n by RVSUM_1:37; :: thesis: x + (- x) = 0* n
hence x + (- x) = 0* n ; :: thesis: verum