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