let IPP be 2-dimensional Desarguesian IncProjSp; :: thesis:
let a, b be POINT of IPP; :: thesis:
let A, B, C, Q, O be LINE of IPP; :: thesis:
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 & not B,C,O are_concurrent ) ; :: thesis:
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 C & d on B ) by INCPROJ:def 14;
consider O1 being LINE of IPP such that
A4: ( a on O1 & d on O1 ) by INCPROJ:def 10;
consider O3 being LINE of IPP such that
A5: ( b on O3 & d on O3 ) by INCPROJ:def 10;
consider p being POINT of IPP such that
A6: ( p on A & p on O1 ) by INCPROJ:def 14;
consider pp' being POINT of IPP such that
A7: ( pp' on O3 & pp' on Q ) by INCPROJ:def 14;
consider O2 being LINE of IPP such that
A8: ( p on O2 & pp' on O2 ) by INCPROJ:def 10;
consider q being POINT of IPP such that
A9: ( q on O & q on O2 ) by INCPROJ:def 14;

assume A10: Q <> C ; :: thesis:
then ( 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 & not B,C,O are_concurrent & A <> Q & Q <> C & a <> b & {c,p} on A & d on B & {c,d} on C & {a,b,q} on O & {c,pp'} on Q & {a,d,p} on O1 & {q,p,pp'} on O2 & {b,d,pp'} on O3 ) by A1, A2, A3, A4, A5, A6, A7, A8, A9, INCSP_1:11, INCSP_1:12;
then A11: ( q <> a & q <> b & not q on A & not q on Q ) by Th17;
take q = q; :: thesis:
(IncProj C,b,B) * (IncProj A,a,C) = (IncProj Q,b,B) * (IncProj A,q,Q) by A1, A2, A3, A4, A5, A6, A7, A8, A9, A10, A11, Th15;
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 A9, A11; :: thesis:

end;

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 A1; :: thesis: