theorem Th29: :: ANPROJ_2:29

for V being non trivial RealLinearSpace st ex u, v, w being Element of V st
( ( for a, b, c being Real st ((a * u) + (b * v)) + (c * w) = 0. V holds
( a = 0 & b = 0 & c = 0 ) ) & ( for y being Element of V ex a, b, c being Real st y = ((a * u) + (b * v)) + (c * w) ) ) holds
ex CS being CollProjectiveSpace st
( CS = ProjectiveSpace V & CS is 2-dimensional )