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) and
A2: 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:
A3: ( not u is zero & not v is zero ) by A2, Th2;
A4: not y is zero by A2, Th2;
then reconsider p = Dir y, q1 = Dir u, q2 = Dir v as Element of (ProjectiveSpace V) by A3, ANPROJ_1:26;
take p ; :: thesis:
take q1 ; :: thesis:
take q2 ; :: thesis:
A5: not y,u,v are_LinDep by A2, Th2;

assume p,q1,q2 is_collinear ; :: thesis:
then [p,q1,q2] in the Collinearity of (ProjectiveSpace V) by COLLSP:def 2;
hence contradiction by A4, A3, A5, ANPROJ_1:25; :: 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
A6: not u1 is zero and
A7: r1 = Dir u1 by ANPROJ_1:26;
consider u2 being Element of V such that
A8: not u2 is zero and
A9: r2 = Dir u2 by ANPROJ_1:26;
consider w1, w2 being Element of V such that
A10: u1,u2,w2 are_LinDep and
A11: u,v,w1 are_LinDep and
A12: y,w2,w1 are_LinDep and
A13: not w1 is zero and
A14: not w2 is zero by A1, A2, A6, A8, Th4;
reconsider q3 = Dir w1, r3 = Dir w2 as Element of (ProjectiveSpace V) by A13, A14, ANPROJ_1:26;
take q3 ; :: thesis:
take r3 ; :: thesis:
thus r1,r2,r3 is_collinear by A6, A7, A8, A9, A10, A14, Th24; :: thesis:
thus q1,q2,q3 is_collinear by A3, A11, A13, Th24; :: thesis:
thus p,r3,q3 is_collinear by A4, A12, A13, A14, Th24; :: thesis: