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

let p, p1, p2, r, r1 be Element of (); :: thesis: ( not p,p1,p2 are_collinear & p,p1,r are_collinear & p1,p2,r1 are_collinear implies ex r2 being Element of () 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 () 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 ;
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 ;
are_Prop v1,v by ;
then A18: v,w,s are_LinDep by ;
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 ;
reconsider r2 = Dir y as Element of () by ;
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