let F be Field; :: thesis: for a, b, c being Element of F holds a - ((a + b) + (- c)) = c - b
let a, b, c be Element of F; :: thesis: a - ((a + b) + (- c)) = c - b
thus a - ((a + b) + (- c)) = a - (a + (b + (- c))) by RLVECT_1:def 3
.= a - (a + (b - c)) by RLVECT_1:def 11
.= a + (- (a + (b - c))) by RLVECT_1:def 11
.= a + ((- a) + (- (b - c))) by RLVECT_1:31
.= (a + (- a)) + (- (b - c)) by RLVECT_1:def 3
.= (0. F) + (- (b - c)) by RLVECT_1:def 10
.= - (b - c) by RLVECT_1:4
.= c - b by Lm1 ; :: thesis: verum