let V be non trivial RealLinearSpace; :: thesis: for p, p1, p2, r, r1 being Element of (ProjectiveSpace V) st not p,p1,p2 are_collinear & p,p1,r are_collinear & p1,p2,r1 are_collinear holds

ex r2 being Element of (ProjectiveSpace V) st

( p,p2,r2 are_collinear & r,r1,r2 are_collinear )

let p, p1, p2, r, r1 be Element of (ProjectiveSpace V); :: thesis: ( not p,p1,p2 are_collinear & p,p1,r are_collinear & p1,p2,r1 are_collinear implies ex r2 being Element of (ProjectiveSpace V) st

( p,p2,r2 are_collinear & r,r1,r2 are_collinear ) )

assume that

A1: not p,p1,p2 are_collinear and

A2: p,p1,r are_collinear and

A3: p1,p2,r1 are_collinear ; :: thesis: ex r2 being Element of (ProjectiveSpace V) st

( p,p2,r2 are_collinear & r,r1,r2 are_collinear )

consider u, v, t being Element of V such that

A4: p = Dir u and

A5: p1 = Dir v and

A6: r = Dir t and

A7: not u is zero and

A8: not v is zero and

A9: not t is zero and

A10: u,v,t are_LinDep by A2, Th23;

consider v1, w, s being Element of V such that

A11: p1 = Dir v1 and

A12: p2 = Dir w and

A13: r1 = Dir s and

A14: not v1 is zero and

A15: not w is zero and

A16: not s is zero and

A17: v1,w,s are_LinDep by A3, Th23;

are_Prop v1,v by A5, A8, A11, A14, ANPROJ_1:22;

then A18: v,w,s are_LinDep by A17, ANPROJ_1:4;

not u,v,w are_LinDep by A1, A4, A5, A7, A8, A12, A15, Th23;

then consider y being Element of V such that

A19: ( u,w,y are_LinDep & t,s,y are_LinDep ) and

A20: not y is zero by A10, A18, ANPROJ_1:15;

reconsider r2 = Dir y as Element of (ProjectiveSpace V) by A20, ANPROJ_1:26;

take r2 ; :: thesis: ( p,p2,r2 are_collinear & r,r1,r2 are_collinear )

thus ( p,p2,r2 are_collinear & r,r1,r2 are_collinear ) by A4, A6, A7, A9, A12, A13, A15, A16, A19, A20, Th23; :: thesis: verum

ex r2 being Element of (ProjectiveSpace V) st

( p,p2,r2 are_collinear & r,r1,r2 are_collinear )

let p, p1, p2, r, r1 be Element of (ProjectiveSpace V); :: thesis: ( not p,p1,p2 are_collinear & p,p1,r are_collinear & p1,p2,r1 are_collinear implies ex r2 being Element of (ProjectiveSpace V) st

( p,p2,r2 are_collinear & r,r1,r2 are_collinear ) )

assume that

A1: not p,p1,p2 are_collinear and

A2: p,p1,r are_collinear and

A3: p1,p2,r1 are_collinear ; :: thesis: ex r2 being Element of (ProjectiveSpace V) st

( p,p2,r2 are_collinear & r,r1,r2 are_collinear )

consider u, v, t being Element of V such that

A4: p = Dir u and

A5: p1 = Dir v and

A6: r = Dir t and

A7: not u is zero and

A8: not v is zero and

A9: not t is zero and

A10: u,v,t are_LinDep by A2, Th23;

consider v1, w, s being Element of V such that

A11: p1 = Dir v1 and

A12: p2 = Dir w and

A13: r1 = Dir s and

A14: not v1 is zero and

A15: not w is zero and

A16: not s is zero and

A17: v1,w,s are_LinDep by A3, Th23;

are_Prop v1,v by A5, A8, A11, A14, ANPROJ_1:22;

then A18: v,w,s are_LinDep by A17, ANPROJ_1:4;

not u,v,w are_LinDep by A1, A4, A5, A7, A8, A12, A15, Th23;

then consider y being Element of V such that

A19: ( u,w,y are_LinDep & t,s,y are_LinDep ) and

A20: not y is zero by A10, A18, ANPROJ_1:15;

reconsider r2 = Dir y as Element of (ProjectiveSpace V) by A20, ANPROJ_1:26;

take r2 ; :: thesis: ( p,p2,r2 are_collinear & r,r1,r2 are_collinear )

thus ( p,p2,r2 are_collinear & r,r1,r2 are_collinear ) by A4, A6, A7, A9, A12, A13, A15, A16, A19, A20, Th23; :: thesis: verum