let V be non trivial RealLinearSpace; :: 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 ) ) ) implies for p, p1, q, q1 being Element of () ex r being Element of () st
( p,p1,r are_collinear & q,q1,r are_collinear ) )

given x1, x2 being Element of () such that A1: x1 <> x2 and
A2: for r1, r2 being Element of () ex q being Element of () st
( x1,x2,q are_collinear & r1,r2,q are_collinear ) ; :: thesis: for p, p1, q, q1 being Element of () ex r being Element of () st
( p,p1,r are_collinear & q,q1,r are_collinear )

let p, p1, q, q1 be Element of (); :: thesis: ex r being Element of () st
( p,p1,r are_collinear & q,q1,r are_collinear )

consider p3 being Element of () such that
A3: x1,x2,p3 are_collinear and
A4: p,p1,p3 are_collinear by A2;
consider q3 being Element of () such that
A5: x1,x2,q3 are_collinear and
A6: q,q1,q3 are_collinear by A2;
consider s2 being Element of () such that
A7: x1,x2,s2 are_collinear and
A8: p,q,s2 are_collinear by A2;
A9: s2,p,q are_collinear by ;
consider s4 being Element of () such that
A10: x1,x2,s4 are_collinear and
A11: p,q1,s4 are_collinear by A2;
A12: s4,q1,p are_collinear by ;
p3,s2,q3 are_collinear by A1, A3, A5, A7, Def8;
then consider s3 being Element of () such that
A13: p3,p,s3 are_collinear and
A14: q3,q,s3 are_collinear by ;
consider s being Element of () such that
A15: x1,x2,s are_collinear and
A16: p1,q1,s are_collinear by A2;
q3,s4,p3 are_collinear by A1, A3, A5, A10, Def8;
then consider s5 being Element of () such that
A17: q3,q1,s5 are_collinear and
A18: p3,p,s5 are_collinear by ;
A19: p1,s,q1 are_collinear by ;
consider s6 being Element of () such that
A20: x1,x2,s6 are_collinear and
A21: p1,q,s6 are_collinear by A2;
A22: s6,p1,q are_collinear by ;
p3,s6,q3 are_collinear by A1, A3, A5, A20, Def8;
then consider s7 being Element of () such that
A23: p3,p1,s7 are_collinear and
A24: q3,q,s7 are_collinear by ;
s,p3,q3 are_collinear by A1, A3, A5, A15, Def8;
then consider s1 being Element of () such that
A25: p1,p3,s1 are_collinear and
A26: q1,q3,s1 are_collinear by ;
A27: now :: thesis: ( p <> p1 & q <> q1 implies ex r being Element of () st
( p,p1,r are_collinear & q,q1,r are_collinear ) )
A28: now :: thesis: ( p3 <> p1 & q3 <> q1 implies ex s1, r being Element of () st
( p,p1,r are_collinear & q,q1,r are_collinear ) )
end;
A34: now :: thesis: ( p3 <> p & q3 <> q implies ex s3, r being Element of () st
( p,p1,r are_collinear & q,q1,r are_collinear ) )
assume that
A35: p3 <> p and
A36: q3 <> q ; :: thesis: ex s3, r being Element of () st
( p,p1,r are_collinear & q,q1,r are_collinear )

take s3 = s3; :: thesis: ex r being Element of () st
( p,p1,r are_collinear & q,q1,r are_collinear )

( q3,q,q are_collinear & q3,q,q1 are_collinear ) by ;
then A37: q,q1,s3 are_collinear by ;
( p3,p,p are_collinear & p3,p,p1 are_collinear ) by ;
then p,p1,s3 are_collinear by ;
hence ex r being Element of () st
( p,p1,r are_collinear & q,q1,r are_collinear ) by A37; :: thesis: verum
end;
A38: now :: thesis: ( p3 <> p1 & q3 <> q implies ex s7, r being Element of () st
( p,p1,r are_collinear & q,q1,r are_collinear ) )
assume that
A39: p3 <> p1 and
A40: q3 <> q ; :: thesis: ex s7, r being Element of () st
( p,p1,r are_collinear & q,q1,r are_collinear )

take s7 = s7; :: thesis: ex r being Element of () st
( p,p1,r are_collinear & q,q1,r are_collinear )

( q3,q,q are_collinear & q3,q,q1 are_collinear ) by ;
then A41: q,q1,s7 are_collinear by ;
( p3,p1,p are_collinear & p3,p1,p1 are_collinear ) by ;
then p,p1,s7 are_collinear by ;
hence ex r being Element of () st
( p,p1,r are_collinear & q,q1,r are_collinear ) by A41; :: thesis: verum
end;
A42: now :: thesis: ( p3 <> p & q3 <> q1 implies ex s5, r being Element of () st
( p,p1,r are_collinear & q,q1,r are_collinear ) )
assume that
A43: p3 <> p and
A44: q3 <> q1 ; :: thesis: ex s5, r being Element of () st
( p,p1,r are_collinear & q,q1,r are_collinear )

take s5 = s5; :: thesis: ex r being Element of () st
( p,p1,r are_collinear & q,q1,r are_collinear )

( q3,q1,q are_collinear & q3,q1,q1 are_collinear ) by ;
then A45: q,q1,s5 are_collinear by ;
( p3,p,p are_collinear & p3,p,p1 are_collinear ) by ;
then p,p1,s5 are_collinear by ;
hence ex r being Element of () st
( p,p1,r are_collinear & q,q1,r are_collinear ) by A45; :: thesis: verum
end;
assume ( p <> p1 & q <> q1 ) ; :: thesis: ex r being Element of () st
( p,p1,r are_collinear & q,q1,r are_collinear )

hence ex r being Element of () st
( p,p1,r are_collinear & q,q1,r are_collinear ) by A34, A42, A38, A28; :: thesis: verum
end;
now :: thesis: ( ( p = p1 or q = q1 ) implies ex r being Element of () st
( p,p1,r are_collinear & q,q1,r are_collinear ) )
A46: now :: thesis: ( p = p1 implies ex q3, r being Element of () st
( p,p1,r are_collinear & q,q1,r are_collinear ) )
assume A47: p = p1 ; :: thesis: ex q3, r being Element of () st
( p,p1,r are_collinear & q,q1,r are_collinear )

take q3 = q3; :: thesis: ex r being Element of () st
( p,p1,r are_collinear & q,q1,r are_collinear )

p,p1,q3 are_collinear by ;
hence ex r being Element of () st
( p,p1,r are_collinear & q,q1,r are_collinear ) by A6; :: thesis: verum
end;
A48: now :: thesis: ( q = q1 implies ex p3, r being Element of () st
( p,p1,r are_collinear & q,q1,r are_collinear ) )
assume A49: q = q1 ; :: thesis: ex p3, r being Element of () st
( p,p1,r are_collinear & q,q1,r are_collinear )

take p3 = p3; :: thesis: ex r being Element of () st
( p,p1,r are_collinear & q,q1,r are_collinear )

q,q1,p3 are_collinear by ;
hence ex r being Element of () st
( p,p1,r are_collinear & q,q1,r are_collinear ) by A4; :: thesis: verum
end;
assume ( p = p1 or q = q1 ) ; :: thesis: ex r being Element of () st
( p,p1,r are_collinear & q,q1,r are_collinear )

hence ex r being Element of () st
( p,p1,r are_collinear & q,q1,r are_collinear ) by ; :: thesis: verum
end;
hence ex r being Element of () st
( p,p1,r are_collinear & q,q1,r are_collinear ) by A27; :: thesis: verum