let IPP be 2-dimensional Desarguesian IncProjSp; :: thesis: for a, b, c, q being POINT of IPP
for A, B, C, O being LINE of IPP st 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 holds
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)) )
let a, b, c, q be POINT of IPP; :: thesis: for A, B, C, O being LINE of IPP st 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 holds
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)) )
let A, B, C, O be LINE of IPP; :: thesis: ( 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 implies 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)) ) )
assume that
A1: not a on A and
A2: not b on B and
A3: ( not a on C & not b on C ) and
A4: c on A and
A5: c on C and
A6: a <> b and
A7: ( a on O & b on O & q on O ) and
A8: not q on A and
A9: q <> b and
A10: ( not A,B,C are_concurrent & not B,C,O are_concurrent ) ; :: thesis: 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)) )
consider d being POINT of IPP such that
A11: d on C and
A12: d on B by INCPROJ:def 9;
consider O1 being LINE of IPP such that
A13: ( a on O1 & d on O1 ) by INCPROJ:def 5;
consider O3 being LINE of IPP such that
A14: ( b on O3 & d on O3 ) by INCPROJ:def 5;
consider p being POINT of IPP such that
A15: p on A and
A16: p on O1 by INCPROJ:def 9;
consider O2 being LINE of IPP such that
A17: ( q on O2 & p on O2 ) by INCPROJ:def 5;
consider pp9 being POINT of IPP such that
A18: pp9 on O3 and
A19: pp9 on O2 by INCPROJ:def 9;
consider Q being LINE of IPP such that
A20: c on Q and
A21: pp9 on Q by INCPROJ:def 5;

now :: thesis: ( q <> a implies 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)) ) )

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

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 A3, A5; :: thesis: verum