let CPS be CollProjectiveSpace; ( ( 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 )
; 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); 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; verum