consider V being RealLinearSpace, u, v being VECTOR of V such that
A1: for a, b being Real st (a * u) + (b * v) = 0. V holds
( a = 0 & b = 0 ) and
for w being VECTOR of V ex a, b being Real st w = (a * u) + (b * v) by FUNCSDOM:23;
A2: ( ex a, b, c, d being Element of (OASpace V) st
( not a,b // c,d & not a,b // d,c ) & ( for a, b, c being Element of (OASpace V) ex d being Element of (OASpace V) st
( a,b // c,d & a,c // b,d & b <> d ) ) ) by A1, Th23;
A3: for p, a, b, c being Element of (OASpace V) st p <> b & b,p // p,c holds
ex d being Element of (OASpace V) st
( a,p // p,d & a,b // c,d ) by A1, Th23;
( ex a, b being Element of (OASpace V) st a <> b & ( for a, b, c, d, p, q, r, s being Element of (OASpace V) holds
( a,b // c,c & ( a,b // b,a implies a = b ) & ( a <> b & a,b // p,q & a,b // r,s implies p,q // r,s ) & ( a,b // c,d implies b,a // d,c ) & ( a,b // b,c implies a,b // a,c ) & ( not a,b // a,c or a,b // b,c or a,c // c,b ) ) ) ) by A1, Th23;
then ( not OASpace V is trivial & OASpace V is OAffinSpace-like ) by A2, A3, STRUCT_0:def 10;
hence ex b₁ being non trivial AffinStruct st
( b₁ is strict & b₁ is OAffinSpace-like ) ; :: thesis: verum