let V be non trivial RealLinearSpace; :: thesis: ( 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 ) ) ) implies ex CS being CollProjectiveSpace st
( CS = ProjectiveSpace V & CS is at_most-3-dimensional ) )
given y, u, v, w being Element of V such that A1: ( ( 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 ) ) ) ; :: thesis: ex CS being CollProjectiveSpace st
( CS = ProjectiveSpace V & CS is at_most-3-dimensional )
A2: ( ProjectiveSpace V is proper & ProjectiveSpace V is at_least_3rank ) by A1, Lm44;
ex p, q1, q2 being Element of (ProjectiveSpace V) st
( not p,q1,q2 is_collinear & ( for r1, r2 being Element of (ProjectiveSpace V) ex q3, r3 being Element of (ProjectiveSpace V) st
( r1,r2,r3 is_collinear & q1,q2,q3 is_collinear & p,r3,q3 is_collinear ) ) ) by A1, Th32;
hence ex CS being CollProjectiveSpace st
( CS = ProjectiveSpace V & CS is at_most-3-dimensional ) by A2, Th33; :: thesis: verum