consider ADG being Uniquely_Two_Divisible_Group such that
A1: ex a, b being Element of ADG st a <> b by Th11;
( ex a, b being Element of (AV ADG) st a <> b & ( for a, b, c being Element of (AV ADG) st a,b // c,c holds
a = b ) & ( 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 ) & ( for a, b, c, a', b', c' being Element of (AV ADG) st a,b // a',b' & a,c // a',c' holds
b,c // b',c' ) & ( for a, c being Element of (AV ADG) ex b being Element of (AV ADG) st a,b // b,c ) & ( for a, b, c, b' being Element of (AV ADG) st a,b // b,c & a,b' // b',c holds
b = b' ) & ( for a, b, c, d being Element of (AV ADG) st a,b // c,d holds
a,c // b,d ) ) by A1, Th20;
then ( not AV ADG is trivial & AV ADG is AffVect-like ) by Def8, STRUCT_0:def 10;
hence ex b₁ being non empty AffinStruct st
( b₁ is strict & not b₁ is trivial & b₁ is AffVect-like ) ; :: thesis: verum