let IPP be 2-dimensional Desarguesian IncProjSp; for a, b, c, q being POINT of
for A, B, C, O being LINE of 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 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 ; for A, B, C, O being LINE of 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 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 ; ( 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 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 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 such that
A10:
d on B
and
A11:
d on C
and
A12:
d on O
by A9, Def1;
A13:
{a,b,d} on O
by A5, A12, INCSP_1:12;
consider o being POINT of such that
A14:
o on A
and
A15:
o on B
by INCPROJ:def 14;
consider O1 being LINE of such that
A16:
( o on O1 & a on O1 )
by INCPROJ:def 10;
consider o' being POINT of such that
A17:
o' on C
and
A18:
o' on O1
by INCPROJ:def 14;
A19:
{a,o,o'} on O1
by A16, A18, INCSP_1:12;
A20:
{a,o,o'} on O1
by A16, A18, INCSP_1:12;
A21:
{c,d,o'} on C
by A3, A11, A17, INCSP_1:12;
A22:
{c,d,o'} on C
by A3, A11, A17, INCSP_1:12;
consider O2 being LINE of such that
A23:
( b on O2 & o' on O2 )
by INCPROJ:def 10;
A24:
{a,b,d} on O
by A5, A12, INCSP_1:12;
A25:
{c,o} on A
by A2, A14, INCSP_1:11;
A26:
{c,o} on A
by A2, A14, INCSP_1:11;
consider O3 being LINE of such that
A27:
( q on O3 & o on O3 )
by INCPROJ:def 10;
consider o'' being POINT of such that
A28:
o'' on B
and
o'' on O2
by INCPROJ:def 14;
A29:
{o,o'',d} on B
by A10, A15, A28, INCSP_1:12;
consider oo' being POINT of such that
A30:
oo' on O2
and
A31:
oo' on O3
by INCPROJ:def 14;
A32:
{b,o',oo'} on O2
by A23, A30, INCSP_1:12;
A33:
{o,oo',q} on O3
by A27, A31, INCSP_1:12;
A34:
{o,oo',q} on O3
by A27, A31, INCSP_1:12;
A35:
{b,o',oo'} on O2
by A23, A30, INCSP_1:12;
consider Q being LINE of such that
A36:
c on Q
and
A37:
oo' on Q
by INCPROJ:def 10;
A38:
{c,oo'} on Q
by A36, A37, INCSP_1:11;
A39:
{c,oo'} on Q
by A36, A37, INCSP_1:11;
A40:
{o,o'',d} on B
by A10, A15, A28, INCSP_1:12;
then
( not b on Q & A <> Q )
by A1, A4, A6, A7, A8, A25, A21, A13, A38, A19, A32, A34, Th20;
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, Th16;
( not b on Q & not q on Q )
by A1, A4, A6, A7, A8, A25, A40, A21, A13, A38, A19, A32, A34, Th20;
hence
ex Q being LINE of 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