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 are_collinear & p1,q1,r1 are_collinear & r2,r,r1 are_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 are_collinear & p1,q1,r1 are_collinear & r2,r,r1 are_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 M9 = M, N9 = N as LINE of CPS by Th1;
reconsider a9 = a as Point of CPS ;
consider p, q being Point of CPS such that
p <> q and
A2: M9 = Line (p,q) by COLLSP:def 7;
consider p1, q1 being Point of CPS such that
p1 <> q1 and
A3: N9 = Line (p1,q1) by COLLSP:def 7;
consider b9, c9 being Point of CPS such that
A4: p,q,b9 are_collinear and
A5: p1,q1,c9 are_collinear and
A6: a9,b9,c9 are_collinear by A1;
reconsider b = b9, c = c9 as POINT of (IncProjSp_of CPS) ;
b9 in M9 by A2, A4, COLLSP:11;
then A7: b on M by Th5;
c9 in N9 by A3, A5, COLLSP:11;
then A8: c on N by Th5;
ex S being LINE of (IncProjSp_of CPS) st
( a on S & b on S & c on S ) by A6, Th10;
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