let V be non empty right_complementable add-associative right_zeroed addLoopStr ; :: thesis: for v being Element of V holds - (- v) = v
let v be Element of V; :: thesis: - (- v) = v
v + (- v) = 0. V by Def13;
hence - (- v) = v by Th19; :: thesis: verum