let AFV be non empty AffinStruct ; :: thesis: ( AFV is AffVect-like implies AFV is WeakAffVect-like )
assume A1: AFV is AffVect-like ; :: thesis: AFV is WeakAffVect-like
A2: ( ( for a, b, c being Element of ex d being Element of st a,b // c,d ) & ( for a, b, c, a', b', c' being Element of st a,b // a',b' & a,c // a',c' holds
b,c // b',c' ) ) by A1, TDGROUP:def 8;
A3: ( ( for a, c being Element of ex b being Element of st a,b // b,c ) & ( for a, b, c, d being Element of st a,b // c,d holds
a,c // b,d ) ) by A1, TDGROUP:def 8;
( ( for a, b, c being Element of st a,b // c,c holds
a = b ) & ( for a, b, c, d, p, q being Element of st a,b // p,q & c,d // p,q holds
a,b // c,d ) ) by A1, TDGROUP:def 8;
hence AFV is WeakAffVect-like by A2, A3, Def1; :: thesis: verum