let V be non empty right_complementable Abelian add-associative right_zeroed addLoopStr ; :: thesis: for v, u being Element of V holds (v - u) + u = v
let v, u be Element of V; :: thesis: (v - u) + u = v
thus (v - u) + u = v - (u - u) by RLVECT_1:29
.= v - (0. V) by RLVECT_1:5
.= v ; :: thesis: verum