let V be non trivial RealLinearSpace; :: thesis: ( ex u, v, w being Element of V st
( ( for a, b, c being Real st ((a * u) + (b * v)) + (c * w) = 0. V holds
( a = 0 & b = 0 & c = 0 ) ) & ( for y being Element of V ex a, b, c being Real st y = ((a * u) + (b * v)) + (c * w) ) ) implies ex x1, x2 being Element of () st
( x1 <> x2 & ( for r1, r2 being Element of () ex q being Element of () st
( x1,x2,q are_collinear & r1,r2,q are_collinear ) ) ) )

given p, q, r being Element of V such that A1: for a, b, c being Real st ((a * p) + (b * q)) + (c * r) = 0. V holds
( a = 0 & b = 0 & c = 0 ) and
A2: for y being Element of V ex a, b, c being Real st y = ((a * p) + (b * q)) + (c * r) ; :: thesis: ex x1, x2 being Element of () st
( x1 <> x2 & ( for r1, r2 being Element of () ex q being Element of () st
( x1,x2,q are_collinear & r1,r2,q are_collinear ) ) )

A3: ( not p is zero & not q is zero ) by ;
then reconsider x1 = Dir p, x2 = Dir q as Element of () by ANPROJ_1:26;
take x1 ; :: thesis: ex x2 being Element of () st
( x1 <> x2 & ( for r1, r2 being Element of () ex q being Element of () st
( x1,x2,q are_collinear & r1,r2,q are_collinear ) ) )

take x2 ; :: thesis: ( x1 <> x2 & ( for r1, r2 being Element of () ex q being Element of () st
( x1,x2,q are_collinear & r1,r2,q are_collinear ) ) )

not are_Prop p,q by ;
hence x1 <> x2 by ; :: thesis: for r1, r2 being Element of () ex q being Element of () st
( x1,x2,q are_collinear & r1,r2,q are_collinear )

let r1, r2 be Element of (); :: thesis: ex q being Element of () st
( x1,x2,q are_collinear & r1,r2,q are_collinear )

consider u being Element of V such that
A4: ( not u is zero & r1 = Dir u ) by ANPROJ_1:26;
consider u1 being Element of V such that
A5: ( not u1 is zero & r2 = Dir u1 ) by ANPROJ_1:26;
consider y being Element of V such that
A6: p,q,y are_LinDep and
A7: u,u1,y are_LinDep and
A8: not y is zero by A1, A2, Th3;
reconsider q = Dir y as Element of () by ;
take q ; :: thesis: ( x1,x2,q are_collinear & r1,r2,q are_collinear )
thus x1,x2,q are_collinear by A3, A6, A8, Th23; :: thesis: r1,r2,q are_collinear
thus r1,r2,q are_collinear by A4, A5, A7, A8, Th23; :: thesis: verum