v + (- v) = 0. V by Def10;
hence - (- v) = v by Th6; :: thesis: verum