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 6
.= a - (a + (b - c)) by RLVECT_1:def 14
.= a + (- (a + (b - c))) by RLVECT_1:def 14
.= a + ((- a) + (- (b - c))) by RLVECT_1:45
.= (a + (- a)) + (- (b - c)) by RLVECT_1:def 6
.= (0. F) + (- (b - c)) by RLVECT_1:def 13
.= - (b - c) by RLVECT_1:10
.= c - b by Lm1 ; :: thesis: verum