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