let V be non empty right_complementable add-associative right_zeroed addLoopStr ; for v, w being Element of V st v + w = 0. V holds
w + v = 0. V
let v, w be Element of V; ( v + w = 0. V implies w + v = 0. V )
assume A1:
v + w = 0. V
; w + v = 0. V
consider u being Element of V such that
A2:
w + u = 0. V
by ALGSTR_0:def 11;
w + v =
w + (v + (w + u))
by A2, Def4
.=
w + ((v + w) + u)
by Def3
.=
(w + (v + w)) + u
by Def3
.=
w + u
by A1, Def4
;
hence
w + v = 0. V
by A2; verum