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

assume A9: q <> a ; :: thesis:
then ( not a on A & not a on C & not b on B & not b on C & not q on A & not A,B,C are_concurrent & not B,C,O are_concurrent & a <> b & b <> q & q <> a & {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, INCSP_1:11, INCSP_1:12;
then A10: ( Q <> A & Q <> C & not q on Q & not b on Q ) by Th19;
then (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, Th15;
hence ex Q being LINE of IPP st
( c on Q & not b on Q & not q on Q & (IncProj C,b,B) * (IncProj A,a,C) = (IncProj Q,b,B) * (IncProj A,q,Q) ) by A8, A10; :: thesis:

end;

hence ex Q being LINE of IPP st
( c on Q & not b on Q & not q on Q & (IncProj C,b,B) * (IncProj A,a,C) = (IncProj Q,b,B) * (IncProj A,q,Q) ) by A1; :: thesis: