let V be non trivial RealLinearSpace; :: thesis:
given y, u, v, w being Element of V such that A1: ( ( 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 ) ) ) ; :: thesis:
A2: ( not y is zero & not u is zero & not v is zero & not w is zero & not y,u,v are_LinDep ) by A1, Th2;
then reconsider p = Dir y, q1 = Dir u, q2 = Dir v as Element of the carrier of (ProjectiveSpace V) by ANPROJ_1:42;
take p ; :: thesis:
take q1 ; :: thesis:
take q2 ; :: thesis:

assume p,q1,q2 is_collinear ; :: thesis:
then [p,q1,q2] in the Collinearity of (ProjectiveSpace V) by COLLSP:def 2;
hence contradiction by A2, ANPROJ_1:41; :: thesis:

end;

hence not p,q1,q2 is_collinear ; :: thesis:
let r1, r2 be Element of (ProjectiveSpace V); :: thesis:
consider u1 being Element of V such that
A3: ( not u1 is zero & r1 = Dir u1 ) by ANPROJ_1:42;
consider u2 being Element of V such that
A4: ( not u2 is zero & r2 = Dir u2 ) by ANPROJ_1:42;
consider w1, w2 being Element of V such that
A5: ( u1,u2,w2 are_LinDep & u,v,w1 are_LinDep & y,w2,w1 are_LinDep & not w1 is zero & not w2 is zero ) by A1, A3, A4, Th4;
reconsider q3 = Dir w1, r3 = Dir w2 as Element of the carrier of (ProjectiveSpace V) by A5, ANPROJ_1:42;
take q3 ; :: thesis:
take r3 ; :: thesis:
thus r1,r2,r3 is_collinear by A3, A4, A5, Th24; :: thesis:
thus q1,q2,q3 is_collinear by A2, A5, Th24; :: thesis:
thus p,r3,q3 is_collinear by A2, A5, Th24; :: thesis: