let V be non empty right_complementable Abelian 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 Th30
.= (- w) - v by Th30 ; :: thesis: verum