theorem :: AFVECT0:51
for AS being strict AffinStruct holds
( AS is AffVect iff ex ADG being Proper_Uniquely_Two_Divisible_Group st AS = AV ADG )