let CPS be CollProjectiveSpace; :: thesis: ( ( for a9, b9, c9, d9 being Point of CPS ex p9 being Point of CPS st
( a9,b9,p9 are_collinear & c9,d9,p9 are_collinear ) ) implies for M, N being LINE of (IncProjSp_of CPS) ex q being POINT of (IncProjSp_of CPS) st
( q on M & q on N ) )
assume A1: for a9, b9, c9, d9 being Point of CPS ex p9 being Point of CPS st
( a9,b9,p9 are_collinear & c9,d9,p9 are_collinear ) ; :: thesis: for M, N being LINE of (IncProjSp_of CPS) ex q being POINT of (IncProjSp_of CPS) st
( q on M & q on N )
let M, N be LINE of (IncProjSp_of CPS); :: thesis: ex q being POINT of (IncProjSp_of CPS) st
( q on M & q on N )
reconsider M9 = M, N9 = N as LINE of CPS by Th1;
consider a9, b9 being Point of CPS such that
a9 <> b9 and
A2: M9 = Line (a9,b9) by COLLSP:def 7;
consider c9, d9 being Point of CPS such that
c9 <> d9 and
A3: N9 = Line (c9,d9) by COLLSP:def 7;
consider p9 being Point of CPS such that
A4: a9,b9,p9 are_collinear and
A5: c9,d9,p9 are_collinear by A1;
reconsider q = p9 as POINT of (IncProjSp_of CPS) ;
p9 in N9 by A3, A5, COLLSP:11;
then A6: q on N by Th5;
p9 in M9 by A2, A4, COLLSP:11;
then q on M by Th5;
hence ex q being POINT of (IncProjSp_of CPS) st
( q on M & q on N ) by A6; :: thesis: verum