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