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 & 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 & 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 & 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 & not b on B & not a on C & not b on C ) and
A2: c on A and
A3: c on C and
A4: a <> b and
A5: ( a on O & b on O ) and
A6: q on O and
A7: not q on A and
A8: ( q <> b & not A,B,C are_concurrent ) and
A9: 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
A10: d on B and
A11: d on C and
A12: d on O by A9;
A13: {a,b,d} on O by ;
consider o being POINT of IPP such that
A14: o on A and
A15: o on B by INCPROJ:def 9;
consider O1 being LINE of IPP such that
A16: ( o on O1 & a on O1 ) by INCPROJ:def 5;
consider o9 being POINT of IPP such that
A17: o9 on C and
A18: o9 on O1 by INCPROJ:def 9;
A19: {a,o,o9} on O1 by ;
A20: {a,o,o9} on O1 by ;
A21: {c,d,o9} on C by ;
A22: {c,d,o9} on C by ;
consider O2 being LINE of IPP such that
A23: ( b on O2 & o9 on O2 ) by INCPROJ:def 5;
A24: {a,b,d} on O by ;
A25: {c,o} on A by ;
A26: {c,o} on A by ;
consider O3 being LINE of IPP such that
A27: ( q on O3 & o on O3 ) by INCPROJ:def 5;
consider o99 being POINT of IPP such that
A28: o99 on B and
o99 on O2 by INCPROJ:def 9;
A29: {o,o99,d} on B by ;
consider oo9 being POINT of IPP such that
A30: oo9 on O2 and
A31: oo9 on O3 by INCPROJ:def 9;
A32: {b,o9,oo9} on O2 by ;
A33: {o,oo9,q} on O3 by ;
A34: {o,oo9,q} on O3 by ;
A35: {b,o9,oo9} on O2 by ;
consider Q being LINE of IPP such that
A36: c on Q and
A37: oo9 on Q by INCPROJ:def 5;
A38: {c,oo9} on Q by ;
A39: {c,oo9} on Q by ;
A40: {o,o99,d} on B by ;
then ( not b on Q & A <> Q ) by A1, A4, A6, A7, A8, A25, A21, A13, A38, A19, A32, A34, Th19;
then A41: (IncProj (C,b,B)) * (IncProj (A,a,C)) = (IncProj (Q,b,B)) * (IncProj (A,q,Q)) by A1, A4, A6, A8, A26, A29, A22, A24, A39, A20, A35, A33, Th15;
( not b on Q & not q on Q ) by A1, A4, A6, A7, A8, A25, A40, A21, A13, A38, A19, A32, A34, Th19;
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 ; :: thesis: verum