let n be Nat; :: thesis: for x1, x2, x3 being Element of REAL n holds x1 - (x2 - x3) = (x1 - x2) + x3
let x1, x2, x3 be Element of REAL n; :: thesis: x1 - (x2 - x3) = (x1 - x2) + x3
thus x1 - (x2 - x3) = (x1 - x2) - (- x3) by RVSUM_1:39
.= (x1 - x2) + x3 ; :: thesis: verum