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 & not 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 & not 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 & not 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
and
A2:
not b on B
and
A3:
not a on C
and
A4:
( not b on C & not A,B,C are_concurrent )
and
A5:
A,C,Q are_concurrent
and
A6:
( not b on Q & A <> Q )
and
A7:
a <> b
and
A8:
a on O
and
A9:
b on O
and
A10:
not 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 c being POINT of IPP such that
A11:
( c on A & c on C )
and
A12:
c on Q
by A5;
consider d being POINT of IPP such that
A13:
d on C
and
A14:
d on B
by INCPROJ:def 9;
consider O1 being LINE of IPP such that
A15:
( a on O1 & d on O1 )
by INCPROJ:def 5;
consider O3 being LINE of IPP such that
A16:
( b on O3 & d on O3 )
by INCPROJ:def 5;
consider pp9 being POINT of IPP such that
A17:
pp9 on O3
and
A18:
pp9 on Q
by INCPROJ:def 9;
consider p being POINT of IPP such that
A19:
p on A
and
A20:
p on O1
by INCPROJ:def 9;
consider O2 being LINE of IPP such that
A21:
( p on O2 & pp9 on O2 )
by INCPROJ:def 5;
consider q being POINT of IPP such that
A22:
q on O
and
A23:
q on O2
by INCPROJ:def 9;
now ( Q <> C implies ex q, 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 A24:
Q <> C
;
ex q, 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)) )take q =
q;
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)) )A25:
{b,d,pp9} on O3
by A16, A17, INCSP_1:2;
A26:
(
{a,d,p} on O1 &
{q,p,pp9} on O2 )
by A15, A20, A21, A23, INCSP_1:2;
A27:
(
{c,p} on A &
{c,d} on C )
by A11, A13, A19, INCSP_1:1;
A28:
(
{a,b,q} on O &
{c,pp9} on Q )
by A8, A9, A12, A18, A22, INCSP_1:1, INCSP_1:2;
then A29:
( not
q on A & not
q on Q )
by A1, A3, A4, A6, A7, A10, A14, A24, A27, A26, A25, Th16;
q <> a
by A1, A3, A4, A6, A7, A10, A14, A24, A27, A28, A26, A25, Th16;
then
(IncProj (C,b,B)) * (IncProj (A,a,C)) = (IncProj (Q,b,B)) * (IncProj (A,q,Q))
by A1, A2, A3, A4, A6, A8, A9, A10, A11, A12, A13, A14, A15, A16, A19, A20, A17, A18, A21, A22, A23, A29, Th14;
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 A22, A29;
verum end;
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 A1, A3, A8; verum