let ADG be Proper_Uniquely_Two_Divisible_Group; :: thesis: AV ADG is AffVect
ex a, b being Element of ADG st a <> b by STRUCT_0:def 10;
hence AV ADG is AffVect by TDGROUP:17; :: thesis: verum