let IPP be 2-dimensional Desarguesian IncProjSp; :: thesis: for a, b being POINT of IPP
for A, B, C, Q, O being LINE of IPP st not a on A & not b on B & not a on C & not b on C & not A,B,C are_concurrent & A,C,Q are_concurrent & not b on Q & A <> Q & a <> b & a on O & b on O & B,C,O are_concurrent holds
ex q being POINT of IPP st
( q on O & not q on A & not q on Q & (IncProj C,b,B) * (IncProj A,a,C) = (IncProj Q,b,B) * (IncProj A,q,Q) )
let a, b be POINT of IPP; :: thesis: for A, B, C, Q, O being LINE of IPP st not a on A & not b on B & not a on C & not b on C & not A,B,C are_concurrent & A,C,Q are_concurrent & not b on Q & A <> Q & a <> b & a on O & b on O & B,C,O are_concurrent holds
ex q being POINT of IPP st
( q on O & not q on A & not q on Q & (IncProj C,b,B) * (IncProj A,a,C) = (IncProj Q,b,B) * (IncProj A,q,Q) )
let A, B, C, Q, O be LINE of IPP; :: thesis: ( not a on A & not b on B & not a on C & not b on C & not A,B,C are_concurrent & A,C,Q are_concurrent & not b on Q & A <> Q & a <> b & a on O & b on O & B,C,O are_concurrent implies ex q being POINT of IPP st
( q on O & not q on A & not q on Q & (IncProj C,b,B) * (IncProj A,a,C) = (IncProj Q,b,B) * (IncProj A,q,Q) ) )
assume A1: ( not a on A & not b on B & not a on C & not b on C & not A,B,C are_concurrent & A,C,Q are_concurrent & not b on Q & A <> Q & a <> b & a on O & b on O & B,C,O are_concurrent ) ; :: thesis: ex q being POINT of IPP st
( q on O & not q on A & not q on Q & (IncProj C,b,B) * (IncProj A,a,C) = (IncProj Q,b,B) * (IncProj A,q,Q) )
then consider c being POINT of IPP such that
A2: ( c on A & c on C & c on Q ) by Def1;
consider d being POINT of IPP such that
A3: ( d on B & d on C & d on O ) by A1, Def1;
consider o being POINT of IPP such that
A4: ( o on A & o on B ) by INCPROJ:def 14;
consider O1 being LINE of IPP such that
A5: ( o on O1 & a on O1 ) by INCPROJ:def 10;
consider o' being POINT of IPP such that
A6: ( o' on C & o' on O1 ) by INCPROJ:def 14;
consider O2 being LINE of IPP such that
A7: ( b on O2 & o' on O2 ) by INCPROJ:def 10;
consider oo' being POINT of IPP such that
A8: ( oo' on Q & oo' on O2 ) by INCPROJ:def 14;
consider O3 being LINE of IPP such that
A9: ( o on O3 & oo' on O3 ) by INCPROJ:def 10;
consider q being POINT of IPP such that
A10: ( q on O3 & q on O ) by INCPROJ:def 14;
consider o'' being POINT of IPP such that
A11: ( o'' on B & o'' on O2 ) by INCPROJ:def 14;
A12: ( not a on A & not a on C & not b on B & not b on C & not b on Q & not A,B,C are_concurrent & a <> b & A <> Q & {c,o} on A & {o,o'',d} on B & {c,d,o'} on C & {a,b,d} on O & {c,oo'} on Q & {a,o,o'} on O1 & {b,o',oo'} on O2 & {o,oo',q} on O3 & q on O ) by A1, A2, A3, A4, A5, A6, A7, A8, A9, A10, A11, INCSP_1:11, INCSP_1:12;
then A13: ( not q on A & not q on Q & b <> q ) by Th18;
( not a on A & not a on C & not b on B & not b on C & not b on Q & not A,B,C are_concurrent & a <> b & b <> q & A <> Q & {c,o} on A & {o,o'',d} on B & {c,d,o'} on C & {a,b,d} on O & {c,oo'} on Q & {a,o,o'} on O1 & {b,o',oo'} on O2 & {o,oo',q} on O3 & q on O ) by A12, Th18;
then (IncProj C,b,B) * (IncProj A,a,C) = (IncProj Q,b,B) * (IncProj A,q,Q) by Th16;
hence ex q being POINT of IPP st
( q on O & not q on A & not q on Q & (IncProj C,b,B) * (IncProj A,a,C) = (IncProj Q,b,B) * (IncProj A,q,Q) ) by A10, A13; :: thesis: verum