let n be Nat; :: thesis: for a, b, c being Element of (TOP-REAL n) holds (c - a) - (b - a) = c - b
let a, b, c be Element of (TOP-REAL n); :: thesis: (c - a) - (b - a) = c - b
thus (c - a) - (b - a) = ((c - a) - b) + a by RLVECT_1:29
.= ((c - a) + a) + (- b) by RLVECT_1:def 3
.= (c + ((- a) + a)) + (- b) by RLVECT_1:def 3
.= (c + (0. (TOP-REAL n))) + (- b) by RLVECT_1:5
.= c - b ; :: thesis: verum