let V be non trivial RealLinearSpace; :: thesis: ( 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 ) implies ex CS being CollProjectiveSpace st

( CS = ProjectiveSpace V & not CS is 2-dimensional ) )

given u, v, u1, v1 being Element of V such that A1: 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 )

V is up-3-dimensional by A1, Lm42;

then reconsider CS = ProjectiveSpace V as CollProjectiveSpace ;

take CS ; :: thesis: ( CS = ProjectiveSpace V & not CS is 2-dimensional )

thus CS = ProjectiveSpace V ; :: thesis: not CS is 2-dimensional

A2: ( not u1 is zero & not v1 is zero ) by A1, Th2;

A3: ( not u is zero & not v is zero ) by A1, Th2;

then reconsider p = Dir u, p1 = Dir v, q = Dir u1, q1 = Dir v1 as Element of CS by A2, ANPROJ_1:26;

take p ; :: according to ANPROJ_2:def 14 :: thesis: ex p1, q, q1 being Element of CS st

for r being Element of CS holds

( not p,p1,r are_collinear or not q,q1,r are_collinear )

take p1 ; :: thesis: ex q, q1 being Element of CS st

for r being Element of CS holds

( not p,p1,r are_collinear or not q,q1,r are_collinear )

take q ; :: thesis: ex q1 being Element of CS st

for r being Element of CS holds

( not p,p1,r are_collinear or not q,q1,r are_collinear )

take q1 ; :: thesis: for r being Element of CS holds

( not p,p1,r are_collinear or not q,q1,r are_collinear )

thus for r being Element of CS holds

( not p,p1,r are_collinear or not q,q1,r are_collinear ) :: thesis: verum

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 ) )

given u, v, u1, v1 being Element of V such that A1: 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 )

V is up-3-dimensional by A1, Lm42;

then reconsider CS = ProjectiveSpace V as CollProjectiveSpace ;

take CS ; :: thesis: ( CS = ProjectiveSpace V & not CS is 2-dimensional )

thus CS = ProjectiveSpace V ; :: thesis: not CS is 2-dimensional

A2: ( not u1 is zero & not v1 is zero ) by A1, Th2;

A3: ( not u is zero & not v is zero ) by A1, Th2;

then reconsider p = Dir u, p1 = Dir v, q = Dir u1, q1 = Dir v1 as Element of CS by A2, ANPROJ_1:26;

take p ; :: according to ANPROJ_2:def 14 :: thesis: ex p1, q, q1 being Element of CS st

for r being Element of CS holds

( not p,p1,r are_collinear or not q,q1,r are_collinear )

take p1 ; :: thesis: ex q, q1 being Element of CS st

for r being Element of CS holds

( not p,p1,r are_collinear or not q,q1,r are_collinear )

take q ; :: thesis: ex q1 being Element of CS st

for r being Element of CS holds

( not p,p1,r are_collinear or not q,q1,r are_collinear )

take q1 ; :: thesis: for r being Element of CS holds

( not p,p1,r are_collinear or not q,q1,r are_collinear )

thus for r being Element of CS holds

( not p,p1,r are_collinear or not q,q1,r are_collinear ) :: thesis: verum

proof

assume
ex r being Element of CS st

( p,p1,r are_collinear & q,q1,r are_collinear ) ; :: thesis: contradiction

then consider r being Element of CS such that

A4: p,p1,r are_collinear and

A5: q,q1,r are_collinear ;

consider y being Element of V such that

A6: not y is zero and

A7: r = Dir y by ANPROJ_1:26;

[q,q1,r] in the Collinearity of (ProjectiveSpace V) by A5;

then A8: u1,v1,y are_LinDep by A2, A6, A7, ANPROJ_1:25;

[p,p1,r] in the Collinearity of (ProjectiveSpace V) by A4;

then u,v,y are_LinDep by A3, A6, A7, ANPROJ_1:25;

hence contradiction by A1, A6, A8, Th5; :: thesis: verum

end;( p,p1,r are_collinear & q,q1,r are_collinear ) ; :: thesis: contradiction

then consider r being Element of CS such that

A4: p,p1,r are_collinear and

A5: q,q1,r are_collinear ;

consider y being Element of V such that

A6: not y is zero and

A7: r = Dir y by ANPROJ_1:26;

[q,q1,r] in the Collinearity of (ProjectiveSpace V) by A5;

then A8: u1,v1,y are_LinDep by A2, A6, A7, ANPROJ_1:25;

[p,p1,r] in the Collinearity of (ProjectiveSpace V) by A4;

then u,v,y are_LinDep by A3, A6, A7, ANPROJ_1:25;

hence contradiction by A1, A6, A8, Th5; :: thesis: verum