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 (ProjectiveSpace V) st

( x1 <> x2 & ( for r1, r2 being Element of (ProjectiveSpace V) ex q being Element of (ProjectiveSpace V) 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 (ProjectiveSpace V) st

( x1 <> x2 & ( for r1, r2 being Element of (ProjectiveSpace V) ex q being Element of (ProjectiveSpace V) st

( x1,x2,q are_collinear & r1,r2,q are_collinear ) ) )

A3: ( not p is zero & not q is zero ) by A1, Th1;

then reconsider x1 = Dir p, x2 = Dir q as Element of (ProjectiveSpace V) by ANPROJ_1:26;

take x1 ; :: thesis: ex x2 being Element of (ProjectiveSpace V) st

( x1 <> x2 & ( for r1, r2 being Element of (ProjectiveSpace V) ex q being Element of (ProjectiveSpace V) st

( x1,x2,q are_collinear & r1,r2,q are_collinear ) ) )

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

( x1,x2,q are_collinear & r1,r2,q are_collinear ) ) )

not are_Prop p,q by A1, Th1;

hence x1 <> x2 by A3, ANPROJ_1:22; :: thesis: for r1, r2 being Element of (ProjectiveSpace V) ex q being Element of (ProjectiveSpace V) st

( x1,x2,q are_collinear & r1,r2,q are_collinear )

let r1, r2 be Element of (ProjectiveSpace V); :: thesis: ex q being Element of (ProjectiveSpace V) 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 (ProjectiveSpace V) by A8, ANPROJ_1:26;

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

( ( 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 (ProjectiveSpace V) st

( x1 <> x2 & ( for r1, r2 being Element of (ProjectiveSpace V) ex q being Element of (ProjectiveSpace V) 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 (ProjectiveSpace V) st

( x1 <> x2 & ( for r1, r2 being Element of (ProjectiveSpace V) ex q being Element of (ProjectiveSpace V) st

( x1,x2,q are_collinear & r1,r2,q are_collinear ) ) )

A3: ( not p is zero & not q is zero ) by A1, Th1;

then reconsider x1 = Dir p, x2 = Dir q as Element of (ProjectiveSpace V) by ANPROJ_1:26;

take x1 ; :: thesis: ex x2 being Element of (ProjectiveSpace V) st

( x1 <> x2 & ( for r1, r2 being Element of (ProjectiveSpace V) ex q being Element of (ProjectiveSpace V) st

( x1,x2,q are_collinear & r1,r2,q are_collinear ) ) )

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

( x1,x2,q are_collinear & r1,r2,q are_collinear ) ) )

not are_Prop p,q by A1, Th1;

hence x1 <> x2 by A3, ANPROJ_1:22; :: thesis: for r1, r2 being Element of (ProjectiveSpace V) ex q being Element of (ProjectiveSpace V) st

( x1,x2,q are_collinear & r1,r2,q are_collinear )

let r1, r2 be Element of (ProjectiveSpace V); :: thesis: ex q being Element of (ProjectiveSpace V) 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 (ProjectiveSpace V) by A8, ANPROJ_1:26;

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