let CPS be CollProjectiveSpace; for a, b, c, d, p being POINT of (IncProjSp_of CPS)
for P, Q, M, N being LINE of (IncProjSp_of CPS) st a on M & b on M & c on N & d on N & p on M & p on N & a on P & c on P & b on Q & d on Q & not p on P & not p on Q & M <> N holds
ex q being POINT of (IncProjSp_of CPS) st
( q on P & q on Q )
let a, b, c, d, p be POINT of (IncProjSp_of CPS); for P, Q, M, N being LINE of (IncProjSp_of CPS) st a on M & b on M & c on N & d on N & p on M & p on N & a on P & c on P & b on Q & d on Q & not p on P & not p on Q & M <> N holds
ex q being POINT of (IncProjSp_of CPS) st
( q on P & q on Q )
let P, Q, M, N be LINE of (IncProjSp_of CPS); ( a on M & b on M & c on N & d on N & p on M & p on N & a on P & c on P & b on Q & d on Q & not p on P & not p on Q & M <> N implies ex q being POINT of (IncProjSp_of CPS) st
( q on P & q on Q ) )
assume that
A1:
a on M
and
A2:
b on M
and
A3:
c on N
and
A4:
d on N
and
A5:
( p on M & p on N )
and
A6:
a on P
and
A7:
c on P
and
A8:
b on Q
and
A9:
d on Q
and
A10:
not p on P
and
A11:
not p on Q
and
A12:
M <> N
; ex q being POINT of (IncProjSp_of CPS) st
( q on P & q on Q )
reconsider a9 = a, b9 = b, c9 = c, d9 = d, p9 = p as Point of CPS ;
( b9,p9,a9 are_collinear & p9,d9,c9 are_collinear )
by A1, A2, A3, A4, A5, Th10;
then consider q9 being Point of CPS such that
A13:
b9,d9,q9 are_collinear
and
A14:
a9,c9,q9 are_collinear
by ANPROJ_2:def 9;
reconsider q = q9 as POINT of (IncProjSp_of CPS) ;
A15:
ex P2 being LINE of (IncProjSp_of CPS) st
( b on P2 & d on P2 & q on P2 )
by A13, Th10;
b <> d
by A2, A4, A5, A8, A11, A12, Th8;
then A16:
q on Q
by A8, A9, A15, Th8;
A17:
ex P1 being LINE of (IncProjSp_of CPS) st
( a on P1 & c on P1 & q on P1 )
by A14, Th10;
a <> c
by A1, A3, A5, A6, A10, A12, Th8;
then
q on P
by A6, A7, A17, Th8;
hence
ex q being POINT of (IncProjSp_of CPS) st
( q on P & q on Q )
by A16; verum