let F be non empty right_complementable add-associative right_zeroed addLoopStr ; :: thesis: for a, b, c being Element of F holds (b + a) - (c + a) = b - c
let a, b, c be Element of F; :: thesis: (b + a) - (c + a) = b - c
thus (b + a) - (c + a) = (b + a) + (- (c + a)) by RLVECT_1:def 11
.= (b + a) + ((- a) + (- c)) by RLVECT_1:31
.= ((b + a) + (- a)) + (- c) by RLVECT_1:def 3
.= (b + (a + (- a))) + (- c) by RLVECT_1:def 3
.= (b + (0. F)) + (- c) by RLVECT_1:def 10
.= b + (- c) by RLVECT_1:4
.= b - c by RLVECT_1:def 11 ; :: thesis: verum