for V being RealLinearSpace st ex p, q being VECTOR of V st
for w being VECTOR of V ex a, b being Real st (a * p) + (b * q) = w holds
for a, b, c, d being Element of (OASpace V) st not a,b // c,d & not a,b // d,c holds
ex t being Element of (OASpace V) st
( ( a,b // a,t or a,b // t,a ) & ( c,d // c,t or c,d // t,c ) )