let L be non empty right_complementable add-associative right_zeroed addLoopStr ; :: thesis: for a, b being Element of L holds (a - b) + b = a
let a, b be Element of L; :: thesis: (a - b) + b = a
thus (a - b) + b = a + ((- b) + b) by RLVECT_1:def 6
.= a + (0. L) by RLVECT_1:16
.= a by RLVECT_1:def 7 ; :: thesis: verum