let IPP be 2-dimensional Desarguesian IncProjSp; 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; 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; ( 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
; 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 A5, A12, INCSP_1:2;
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 A16, A18, INCSP_1:2;
A20:
{a,o,o9} on O1
by A16, A18, INCSP_1:2;
A21:
{c,d,o9} on C
by A3, A11, A17, INCSP_1:2;
A22:
{c,d,o9} on C
by A3, A11, A17, INCSP_1:2;
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 A5, A12, INCSP_1:2;
A25:
{c,o} on A
by A2, A14, INCSP_1:1;
A26:
{c,o} on A
by A2, A14, INCSP_1:1;
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 A10, A15, A28, INCSP_1:2;
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 A23, A30, INCSP_1:2;
A33:
{o,oo9,q} on O3
by A27, A31, INCSP_1:2;
A34:
{o,oo9,q} on O3
by A27, A31, INCSP_1:2;
A35:
{b,o9,oo9} on O2
by A23, A30, INCSP_1:2;
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 A36, A37, INCSP_1:1;
A39:
{c,oo9} on Q
by A36, A37, INCSP_1:1;
A40:
{o,o99,d} on B
by A10, A15, A28, INCSP_1:2;
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 A36, A41; verum