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, 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 ) ) ) implies ex p, q1, q2 being Element of () st
( not p,q1,q2 are_collinear & ( for r1, r2 being Element of () ex q3, r3 being Element of () st
( r1,r2,r3 are_collinear & q1,q2,q3 are_collinear & p,r3,q3 are_collinear ) ) ) )

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: ex p, q1, q2 being Element of () st
( not p,q1,q2 are_collinear & ( for r1, r2 being Element of () ex q3, r3 being Element of () st
( r1,r2,r3 are_collinear & q1,q2,q3 are_collinear & p,r3,q3 are_collinear ) ) )

A3: ( not u is zero & not v is zero ) by ;
A4: not y is zero by ;
then reconsider p = Dir y, q1 = Dir u, q2 = Dir v as Element of () by ;
take p ; :: thesis: ex q1, q2 being Element of () st
( not p,q1,q2 are_collinear & ( for r1, r2 being Element of () ex q3, r3 being Element of () st
( r1,r2,r3 are_collinear & q1,q2,q3 are_collinear & p,r3,q3 are_collinear ) ) )

take q1 ; :: thesis: ex q2 being Element of () st
( not p,q1,q2 are_collinear & ( for r1, r2 being Element of () ex q3, r3 being Element of () st
( r1,r2,r3 are_collinear & q1,q2,q3 are_collinear & p,r3,q3 are_collinear ) ) )

take q2 ; :: thesis: ( not p,q1,q2 are_collinear & ( for r1, r2 being Element of () ex q3, r3 being Element of () st
( r1,r2,r3 are_collinear & q1,q2,q3 are_collinear & p,r3,q3 are_collinear ) ) )

not y,u,v are_LinDep by ;
then not p,q1,q2 are_collinear by ;
hence not p,q1,q2 are_collinear ; :: thesis: for r1, r2 being Element of () ex q3, r3 being Element of () st
( r1,r2,r3 are_collinear & q1,q2,q3 are_collinear & p,r3,q3 are_collinear )

let r1, r2 be Element of (); :: thesis: ex q3, r3 being Element of () st
( r1,r2,r3 are_collinear & q1,q2,q3 are_collinear & p,r3,q3 are_collinear )

consider u1 being Element of V such that
A5: not u1 is zero and
A6: r1 = Dir u1 by ANPROJ_1:26;
consider u2 being Element of V such that
A7: not u2 is zero and
A8: r2 = Dir u2 by ANPROJ_1:26;
consider w1, w2 being Element of V such that
A9: u1,u2,w2 are_LinDep and
A10: u,v,w1 are_LinDep and
A11: y,w2,w1 are_LinDep and
A12: not w1 is zero and
A13: not w2 is zero by A1, A2, A5, A7, Th4;
reconsider q3 = Dir w1, r3 = Dir w2 as Element of () by ;
take q3 ; :: thesis: ex r3 being Element of () st
( r1,r2,r3 are_collinear & q1,q2,q3 are_collinear & p,r3,q3 are_collinear )

take r3 ; :: thesis: ( r1,r2,r3 are_collinear & q1,q2,q3 are_collinear & p,r3,q3 are_collinear )
thus r1,r2,r3 are_collinear by A5, A6, A7, A8, A9, A13, Th23; :: thesis: ( q1,q2,q3 are_collinear & p,r3,q3 are_collinear )
thus q1,q2,q3 are_collinear by A3, A10, A12, Th23; :: thesis: p,r3,q3 are_collinear
thus p,r3,q3 are_collinear by A4, A11, A12, A13, Th23; :: thesis: verum