v = 0. V by STRUCT_0:def 12;
hence - v = v by Th12; :: thesis: verum