let ADG be Uniquely_Two_Divisible_Group; ( ex a, b being Element of ADG st a <> b implies AV ADG is AffVect )
A1:
( ( for a, b, c being Element of (AV ADG) st a,b // c,c holds
a = b ) & ( for a, b, c, b9 being Element of (AV ADG) st a,b // b,c & a,b9 // b9,c holds
b = b9 ) )
by Th15;
assume A2:
ex a, b being Element of ADG st a <> b
; AV ADG is AffVect
then A3:
( ( for a, b, c, a9, b9, c9 being Element of (AV ADG) st a,b // a9,b9 & a,c // a9,c9 holds
b,c // b9,c9 ) & ( for a, c being Element of (AV ADG) ex b being Element of (AV ADG) st a,b // b,c ) )
by Th15;
A4:
for a, b, c, d being Element of (AV ADG) st a,b // c,d holds
a,c // b,d
by A2, Th15;
( ( for a, b, c, d, p, q being Element of (AV ADG) st a,b // p,q & c,d // p,q holds
a,b // c,d ) & ( for a, b, c being Element of (AV ADG) ex d being Element of (AV ADG) st a,b // c,d ) )
by A2, Th15;
hence
AV ADG is AffVect
by A2, A3, A1, A4, Def5, STRUCT_0:def 10; verum