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

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

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

( not p,q1,q2 are_collinear & ( for r1, r2 being Element of (ProjectiveSpace V) ex q3, r3 being Element of (ProjectiveSpace V) st

( r1,r2,r3 are_collinear & q1,q2,q3 are_collinear & p,r3,q3 are_collinear ) ) )

take q1 ; :: thesis: ex q2 being Element of (ProjectiveSpace V) st

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

( r1,r2,r3 are_collinear & q1,q2,q3 are_collinear & p,r3,q3 are_collinear ) ) )

not y,u,v are_LinDep by A2, Th2;

then not p,q1,q2 are_collinear by A4, A3, ANPROJ_1:25;

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

( r1,r2,r3 are_collinear & q1,q2,q3 are_collinear & p,r3,q3 are_collinear )

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

take q3 ; :: thesis: ex r3 being Element of (ProjectiveSpace V) 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

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

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

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

( not p,q1,q2 are_collinear & ( for r1, r2 being Element of (ProjectiveSpace V) ex q3, r3 being Element of (ProjectiveSpace V) st

( r1,r2,r3 are_collinear & q1,q2,q3 are_collinear & p,r3,q3 are_collinear ) ) )

take q1 ; :: thesis: ex q2 being Element of (ProjectiveSpace V) st

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

( r1,r2,r3 are_collinear & q1,q2,q3 are_collinear & p,r3,q3 are_collinear ) ) )

not y,u,v are_LinDep by A2, Th2;

then not p,q1,q2 are_collinear by A4, A3, ANPROJ_1:25;

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

( r1,r2,r3 are_collinear & q1,q2,q3 are_collinear & p,r3,q3 are_collinear )

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

take q3 ; :: thesis: ex r3 being Element of (ProjectiveSpace V) 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