let V be non trivial RealLinearSpace; :: thesis: ( ex u, v, u1, v1 being Element of V st
( ( for w being Element of V ex a, b, a1, b1 being Real st w = (((a * u) + (b * v)) + (a1 * u1)) + (b1 * v1) ) & ( 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 ) ) ) implies ex CS being CollProjectiveSpace st
( CS = ProjectiveSpace V & not CS is 2-dimensional & CS is at_most-3-dimensional ) )
assume A1: ex u, v, u1, v1 being Element of V st
( ( for w being Element of V ex a, b, a1, b1 being Real st w = (((a * u) + (b * v)) + (a1 * u1)) + (b1 * v1) ) & ( 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 ) ) ) ; :: thesis: ex CS being CollProjectiveSpace st
( CS = ProjectiveSpace V & not CS is 2-dimensional & CS is at_most-3-dimensional )
then consider u, v, u1, v1 being Element of V such that
for w being Element of V ex a, b, a1, b1 being Real st w = (((a * u) + (b * v)) + (a1 * u1)) + (b1 * v1) and
A2: 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 ) ;
consider CS1 being CollProjectiveSpace such that
A3: CS1 = ProjectiveSpace V and
A4: not CS1 is 2-dimensional by A2, Th35;
consider CS2 being CollProjectiveSpace such that
A5: CS2 = ProjectiveSpace V and
A6: CS2 is at_most-3-dimensional by A1, Th34;
thus ex CS being CollProjectiveSpace st
( CS = ProjectiveSpace V & not CS is 2-dimensional & CS is at_most-3-dimensional ) by A3, A4, A5, A6; :: thesis: verum