let V be non empty right_complementable add-associative right_zeroed addLoopStr ; :: thesis: for v, w being Element of V holds - (w + (- v)) = v - w
let v, w be Element of V; :: thesis: - (w + (- v)) = v - w
- (w + (- v)) = (- (- v)) - w by RLVECT_1:30;
hence - (w + (- v)) = v - w by RLVECT_1:17; :: thesis: verum