theorem Th32: :: ANPROJ_2:32

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