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 M' = M, N' = N as LINE of CPS by Th2;
reconsider a' = a as Point of CPS ;
consider p, q being Point of CPS such that
p <> q and
A2: M' = Line p,q by COLLSP:def 7;
consider p1, q1 being Point of CPS such that
p1 <> q1 and
A3: N' = Line p1,q1 by COLLSP:def 7;
consider b', c' being Point of CPS such that
A4: p,q,b' is_collinear and
A5: p1,q1,c' is_collinear and
A6: a',b',c' is_collinear by A1;
reconsider b = b', c = c' as POINT of (IncProjSp_of CPS) ;
b' in M' by A2, A4, COLLSP:17;
then A7: b on M by Th9;
c' in N' by A3, A5, COLLSP:17;
then A8: c on N by Th9;
ex S being LINE of (IncProjSp_of CPS) st
( a on S & b on S & c on S ) by A6, 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 A7, A8; :: thesis: verum