let IPP be 2-dimensional Desarguesian IncProjSp; :: thesis: for a, b being POINT of IPP
for A, B, C, O, Q 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 & not 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, O, Q 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 & not 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, O, Q 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 & not 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 that
A1: not a on A and
A2: not b on B and
A3: not a on C and
A4: ( not b on C & not A,B,C are_concurrent ) and
A5: A,C,Q are_concurrent and
A6: ( not b on Q & A <> Q ) and
A7: a <> b and
A8: a on O and
A9: b on O and
A10: not 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)) )

consider c being POINT of IPP such that
A11: ( c on A & c on C ) and
A12: c on Q by A5;
consider d being POINT of IPP such that
A13: d on C and
A14: d on B by INCPROJ:def 9;
consider O1 being LINE of IPP such that
A15: ( a on O1 & d on O1 ) by INCPROJ:def 5;
consider O3 being LINE of IPP such that
A16: ( b on O3 & d on O3 ) by INCPROJ:def 5;
consider pp9 being POINT of IPP such that
A17: pp9 on O3 and
A18: pp9 on Q by INCPROJ:def 9;
consider p being POINT of IPP such that
A19: p on A and
A20: p on O1 by INCPROJ:def 9;
consider O2 being LINE of IPP such that
A21: ( p on O2 & pp9 on O2 ) by INCPROJ:def 5;
consider q being POINT of IPP such that
A22: q on O and
A23: q on O2 by INCPROJ:def 9;
now :: thesis: ( Q <> C implies ex q, 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 A24: Q <> C ; :: thesis: ex q, 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)) )

take q = q; :: 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)) )

A25: {b,d,pp9} on O3 by ;
A26: ( {a,d,p} on O1 & {q,p,pp9} on O2 ) by ;
A27: ( {c,p} on A & {c,d} on C ) by ;
A28: ( {a,b,q} on O & {c,pp9} on Q ) by ;
then A29: ( not q on A & not q on Q ) by A1, A3, A4, A6, A7, A10, A14, A24, A27, A26, A25, Th16;
q <> a by A1, A3, A4, A6, A7, A10, A14, A24, A27, A28, A26, A25, Th16;
then (IncProj (C,b,B)) * (IncProj (A,a,C)) = (IncProj (Q,b,B)) * (IncProj (A,q,Q)) by A1, A2, A3, A4, A6, A8, A9, A10, A11, A12, A13, A14, A15, A16, A19, A20, A17, A18, A21, A22, A23, A29, Th14;
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 ; :: thesis: verum
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, A3, A8; :: thesis: verum