let CPS be CollProjectiveSpace; :: thesis: ( ( for a', b', c', d' being Point of CPS ex p' being Point of CPS st
( a',b',p' is_collinear & c',d',p' is_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 a', b', c', d' being Point of CPS ex p' being Point of CPS st
( a',b',p' is_collinear & c',d',p' is_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 M' = M, N' = N as LINE of CPS by Th2;
consider a', b' being Point of CPS such that
A2: ( a' <> b' & M' = Line a',b' ) by COLLSP:def 7;
consider c', d' being Point of CPS such that
A3: ( c' <> d' & N' = Line c',d' ) by COLLSP:def 7;
consider p' being Point of CPS such that
A4: ( a',b',p' is_collinear & c',d',p' is_collinear ) by A1;
A5: ( p' in M' & p' in N' ) by A2, A3, A4, COLLSP:17;
reconsider q = p' as POINT of (IncProjSp_of CPS) ;
( q on M & q on N ) by A5, Th9;
hence ex q being POINT of (IncProjSp_of CPS) st
( q on M & q on N ) ; :: thesis: verum