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