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 () st
( not a,b // c,d & not a,b // d,c ) & ( for a, b, c being Element of () ex d being Element of () st
( a,b // c,d & a,c // b,d & b <> d ) ) ) by ;
A3: for p, a, b, c being Element of () st p <> b & b,p // p,c holds
ex d being Element of () st
( a,p // p,d & a,b // c,d ) by ;
( ex a, b being Element of () st a <> b & ( for a, b, c, d, p, q, r, s being Element of () 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 ;
then ( not OASpace V is trivial & OASpace V is OAffinSpace-like ) by ;
hence ex b1 being non trivial AffinStruct st
( b1 is strict & b1 is OAffinSpace-like ) ; :: thesis: verum