let V be non empty right_complementable add-associative right_zeroed addLoopStr ; :: thesis: for v, w being Element of V st v + w = 0. V holds
v = - w
let v, w be Element of V; :: thesis: ( v + w = 0. V implies v = - w )
assume v + w = 0. V ; :: thesis: v = - w
then w + v = 0. V by Lm1;
hence v = - w by Def10; :: thesis: verum