let CPS be CollProjectiveSpace; :: thesis: ( ( for p, p1, q, q1, r2 being Point of CPS ex r, r1 being Point of CPS st
( p,q,r is_collinear & p1,q1,r1 is_collinear & r2,r,r1 is_collinear ) ) implies for a being POINT of (IncProjSp_of CPS)
for M, N being LINE of (IncProjSp_of CPS) ex b, c being POINT of (IncProjSp_of CPS) ex S being LINE of (IncProjSp_of CPS) st
( a on S & b on S & c on S & b on M & c on N ) )
assume A1: for p, p1, q, q1, r2 being Point of CPS ex r, r1 being Point of CPS st
( p,q,r is_collinear & p1,q1,r1 is_collinear & r2,r,r1 is_collinear ) ; :: thesis: for a being POINT of (IncProjSp_of CPS)
for M, N being LINE of (IncProjSp_of CPS) ex b, c being POINT of (IncProjSp_of CPS) ex S being LINE of (IncProjSp_of CPS) st
( a on S & b on S & c on S & b on M & c on N )
let a be POINT of (IncProjSp_of CPS); :: thesis: for M, N being LINE of (IncProjSp_of CPS) ex b, c being POINT of (IncProjSp_of CPS) ex S being LINE of (IncProjSp_of CPS) st
( a on S & b on S & c on S & b on M & c on N )
let M, N be LINE of (IncProjSp_of CPS); :: thesis: ex b, c being POINT of (IncProjSp_of CPS) ex S being LINE of (IncProjSp_of CPS) st
( a on S & b on S & c on S & b on M & c on N )
reconsider a' = a as Point of CPS ;
reconsider M' = M, N' = N as LINE of CPS by Th2;
consider p, q being Point of CPS such that
A2: ( p <> q & M' = Line p,q ) by COLLSP:def 7;
consider p1, q1 being Point of CPS such that
A3: ( p1 <> q1 & N' = Line p1,q1 ) by COLLSP:def 7;
consider b', c' being Point of CPS such that
A4: ( p,q,b' is_collinear & p1,q1,c' is_collinear ) and
A5: a',b',c' is_collinear by A1;
reconsider b = b', c = c' as POINT of (IncProjSp_of CPS) ;
( b' in M' & c' in N' ) by A2, A3, A4, COLLSP:17;
then A6: ( b on M & c on N ) by Th9;
ex S being LINE of (IncProjSp_of CPS) st
( a on S & b on S & c on S ) by A5, Th14;
hence ex b, c being POINT of (IncProjSp_of CPS) ex S being LINE of (IncProjSp_of CPS) st
( a on S & b on S & c on S & b on M & c on N ) by A6; :: thesis: verum