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

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