let V be non trivial RealLinearSpace; :: thesis:
given x1, x2 being Element of (ProjectiveSpace V) such that A1: x1 <> x2 and
A2: 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 ) ; :: thesis:
let p, p1, q, q1 be Element of (ProjectiveSpace V); :: thesis:
consider p3 being Element of (ProjectiveSpace V) such that
A3: x1,x2,p3 are_collinear and
A4: p,p1,p3 are_collinear by A2;
consider q3 being Element of (ProjectiveSpace V) such that
A5: x1,x2,q3 are_collinear and
A6: q,q1,q3 are_collinear by A2;
consider s2 being Element of (ProjectiveSpace V) such that
A7: x1,x2,s2 are_collinear and
A8: p,q,s2 are_collinear by A2;
A9: s2,p,q are_collinear by A8, Th24;
consider s4 being Element of (ProjectiveSpace V) such that
A10: x1,x2,s4 are_collinear and
A11: p,q1,s4 are_collinear by A2;
A12: s4,q1,p are_collinear by A11, Th24;
p3,s2,q3 are_collinear by A1, A3, A5, A7, Def8;
then consider s3 being Element of (ProjectiveSpace V) such that
A13: p3,p,s3 are_collinear and
A14: q3,q,s3 are_collinear by A9, Def9;
consider s being Element of (ProjectiveSpace V) 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 (ProjectiveSpace V) such that
A17: q3,q1,s5 are_collinear and
A18: p3,p,s5 are_collinear by A12, Def9;
A19: p1,s,q1 are_collinear by A16, Th24;
consider s6 being Element of (ProjectiveSpace V) such that
A20: x1,x2,s6 are_collinear and
A21: p1,q,s6 are_collinear by A2;
A22: s6,p1,q are_collinear by A21, Th24;
p3,s6,q3 are_collinear by A1, A3, A5, A20, Def8;
then consider s7 being Element of (ProjectiveSpace V) such that
A23: p3,p1,s7 are_collinear and
A24: q3,q,s7 are_collinear by A22, Def9;
s,p3,q3 are_collinear by A1, A3, A5, A15, Def8;
then consider s1 being Element of (ProjectiveSpace V) such that
A25: p1,p3,s1 are_collinear and
A26: q1,q3,s1 are_collinear by A19, Def9;

A27: now :: thesis:

A28: now :: thesis:

A29: q3,q1,s1 are_collinear by A26, Th24;
assume that
A30: p3 <> p1 and
A31: q3 <> q1 ; :: thesis:
( q3,q1,q are_collinear & q3,q1,q1 are_collinear ) by A6, Def7, Th24;
then A32: q,q1,s1 are_collinear by A31, A29, Def8;
take s1 = s1; :: thesis:
A33: p3,p1,s1 are_collinear by A25, Th24;
( p3,p1,p are_collinear & p3,p1,p1 are_collinear ) by A4, Def7, Th24;
then p,p1,s1 are_collinear by A30, A33, Def8;
hence ex r being Element of (ProjectiveSpace V) st
( p,p1,r are_collinear & q,q1,r are_collinear ) by A32; :: thesis:

end;

A34: now :: thesis:

assume that
A35: p3 <> p and
A36: q3 <> q ; :: thesis:
take s3 = s3; :: thesis:
( q3,q,q are_collinear & q3,q,q1 are_collinear ) by A6, Def7, Th24;
then A37: q,q1,s3 are_collinear by A14, A36, Def8;
( p3,p,p are_collinear & p3,p,p1 are_collinear ) by A4, Def7, Th24;
then p,p1,s3 are_collinear by A13, A35, Def8;
hence ex r being Element of (ProjectiveSpace V) st
( p,p1,r are_collinear & q,q1,r are_collinear ) by A37; :: thesis:

end;

A38: now :: thesis:

assume that
A39: p3 <> p1 and
A40: q3 <> q ; :: thesis:
take s7 = s7; :: thesis:
( q3,q,q are_collinear & q3,q,q1 are_collinear ) by A6, Def7, Th24;
then A41: q,q1,s7 are_collinear by A24, A40, Def8;
( p3,p1,p are_collinear & p3,p1,p1 are_collinear ) by A4, Def7, Th24;
then p,p1,s7 are_collinear by A23, A39, Def8;
hence ex r being Element of (ProjectiveSpace V) st
( p,p1,r are_collinear & q,q1,r are_collinear ) by A41; :: thesis:

end;

A42: now :: thesis:

assume that
A43: p3 <> p and
A44: q3 <> q1 ; :: thesis:
take s5 = s5; :: thesis:
( q3,q1,q are_collinear & q3,q1,q1 are_collinear ) by A6, Def7, Th24;
then A45: q,q1,s5 are_collinear by A17, A44, Def8;
( p3,p,p are_collinear & p3,p,p1 are_collinear ) by A4, Def7, Th24;
then p,p1,s5 are_collinear by A18, A43, Def8;
hence ex r being Element of (ProjectiveSpace V) st
( p,p1,r are_collinear & q,q1,r are_collinear ) by A45; :: thesis:

end;

assume ( p <> p1 & q <> q1 ) ; :: thesis:
hence ex r being Element of (ProjectiveSpace V) st
( p,p1,r are_collinear & q,q1,r are_collinear ) by A34, A42, A38, A28; :: thesis:

end;

now :: thesis:

A46: now :: thesis:

assume A47: p = p1 ; :: thesis:
take q3 = q3; :: thesis:
p,p1,q3 are_collinear by A47, Def7;
hence ex r being Element of (ProjectiveSpace V) st
( p,p1,r are_collinear & q,q1,r are_collinear ) by A6; :: thesis:

end;

A48: now :: thesis:

assume A49: q = q1 ; :: thesis:
take p3 = p3; :: thesis:
q,q1,p3 are_collinear by A49, Def7;
hence ex r being Element of (ProjectiveSpace V) st
( p,p1,r are_collinear & q,q1,r are_collinear ) by A4; :: thesis:

end;

assume ( p = p1 or q = q1 ) ; :: thesis:
hence ex r being Element of (ProjectiveSpace V) st
( p,p1,r are_collinear & q,q1,r are_collinear ) by A48, A46; :: thesis:

end;

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