consider V being RealLinearSpace such that
A1: ex u, v being VECTOR of V st
( ( for a, b being Real st (a * u) + (b * v) = 0. V holds
( a = 0 & b = 0 ) ) & ( for w being VECTOR of V ex a, b being Real st w = (a * u) + (b * v) ) ) by FUNCSDOM:23;
reconsider S = OASpace V as OAffinSpace by A1, Th26;
for a, b, c, d being Element of S st not a,b // c,d & not a,b // d,c holds
ex p being Element of S st
( ( a,b // a,p or a,b // p,a ) & ( c,d // c,p or c,d // p,c ) ) by A1, Th24;
then S is 2-dimensional ;
hence ex b₁ being OAffinSpace st
( b₁ is strict & b₁ is 2-dimensional ) ; :: thesis: verum