let L be non empty right_complementable Abelian add-associative right_zeroed addLoopStr ; :: thesis: for a, b, c being Element of L holds (a - b) - (c - b) = a - c
let a, b, c be Element of L; :: thesis: (a - b) - (c - b) = a - c
thus (a - b) - (c - b) = ((a - b) - c) + b by RLVECT_1:29
.= ((a - b) + b) - c by RLVECT_1:28
.= (a - (b - b)) - c by RLVECT_1:29
.= (a - (0. L)) - c by RLVECT_1:15
.= a - c by RLVECT_1:13 ; :: thesis: verum