theorem Th33: :: ANPROJ_2:33

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