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