let V be RealLinearSpace; :: thesis: ( 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) ) ) implies OASpace V is OAffinPlane )

set S = OASpace V;

assume 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) ) ) ; :: thesis: OASpace V is OAffinPlane

then for a, b, c, d being Element of (OASpace V) st not a,b // c,d & not a,b // d,c holds

ex p being Element of (OASpace V) st

( ( a,b // a,p or a,b // p,a ) & ( c,d // c,p or c,d // p,c ) ) by Th24;

hence OASpace V is OAffinPlane by A1, Def6, Th26; :: thesis: verum

( ( 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) ) ) implies OASpace V is OAffinPlane )

set S = OASpace V;

assume 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) ) ) ; :: thesis: OASpace V is OAffinPlane

then for a, b, c, d being Element of (OASpace V) st not a,b // c,d & not a,b // d,c holds

ex p being Element of (OASpace V) st

( ( a,b // a,p or a,b // p,a ) & ( c,d // c,p or c,d // p,c ) ) by Th24;

hence OASpace V is OAffinPlane by A1, Def6, Th26; :: thesis: verum