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)
thus - (v - w) = (- (- w)) + (- v) by Lm3
.= w + (- v) ; :: thesis: verum