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