let CPS be CollProjectiveSpace; for a, b, c, d, p being POINT of
for M, N, P, Q being LINE of 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 st
( q on P & q on Q )
let a, b, c, d, p be POINT of ; for M, N, P, Q being LINE of 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 st
( q on P & q on Q )
let M, N, P, Q be LINE of ; ( 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 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 st
( q on P & q on Q )
reconsider a' = a, b' = b, c' = c, d' = d, p' = p as Point of ;
( b',p',a' is_collinear & p',d',c' is_collinear )
by A1, A2, A3, A4, A5, Th14;
then consider q' being Point of such that
A13:
b',d',q' is_collinear
and
A14:
a',c',q' is_collinear
by ANPROJ_2:def 9;
reconsider q = q' as POINT of ;
A15:
ex P2 being LINE of st
( b on P2 & d on P2 & q on P2 )
by A13, Th14;
b <> d
by A2, A4, A5, A8, A11, A12, Th12;
then A16:
q on Q
by A8, A9, A15, Th12;
A17:
ex P1 being LINE of st
( a on P1 & c on P1 & q on P1 )
by A14, Th14;
a <> c
by A1, A3, A5, A6, A10, A12, Th12;
then
q on P
by A6, A7, A17, Th12;
hence
ex q being POINT of st
( q on P & q on Q )
by A16; verum