set AFV = the strict AffVect;
reconsider AS = the strict AffVect as non empty AffinStruct ;
A1: ( ( for a, b, c being Element of AS ex d being Element of AS st a,b // c,d ) & ( for a, b, c, a9, b9, c9 being Element of AS st a,b // a9,b9 & a,c // a9,c9 holds
b,c // b9,c9 ) ) by TDGROUP:16;
A2: ( ( for a, c being Element of AS ex b being Element of AS st a,b // b,c ) & ( for a, b, c, d being Element of AS st a,b // c,d holds
a,c // b,d ) ) by TDGROUP:16;
( ( for a, b, c being Element of AS st a,b // c,c holds
a = b ) & ( for a, b, c, d, p, q being Element of AS st a,b // p,q & c,d // p,q holds
a,b // c,d ) ) by TDGROUP:16;
then AS is WeakAffVect-like by A1, A2;
hence ex b₁ being non trivial AffinStruct st
( b₁ is strict & b₁ is WeakAffVect-like ) ; :: thesis: verum