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