theorem Th30: :: ANPROJ_2:30

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, a1, b1 being Real st w1 = (((a * y) + (b * u)) + (a1 * v)) + (b1 * 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 p, q1, q2 being Element of (ProjectiveSpace V) st
( not p,q1,q2 are_collinear & ( for r1, r2 being Element of (ProjectiveSpace V) ex q3, r3 being Element of (ProjectiveSpace V) st
( r1,r2,r3 are_collinear & q1,q2,q3 are_collinear & p,r3,q3 are_collinear ) ) )