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 & B,C,Q are_concurrent & not a on Q & B <> Q & a <> b & a on O & b on O holds
ex q being POINT of IPP st
( q on O & not q on B & not q on Q & (IncProj (C,b,B)) * (IncProj (A,a,C)) = (IncProj (Q,q,B)) * (IncProj (A,a,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 & B,C,Q are_concurrent & not a on Q & B <> Q & a <> b & a on O & b on O holds
ex q being POINT of IPP st
( q on O & not q on B & not q on Q & (IncProj (C,b,B)) * (IncProj (A,a,C)) = (IncProj (Q,q,B)) * (IncProj (A,a,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 & B,C,Q are_concurrent & not a on Q & B <> Q & a <> b & a on O & b on O implies ex q being POINT of IPP st
( q on O & not q on B & not q on Q & (IncProj (C,b,B)) * (IncProj (A,a,C)) = (IncProj (Q,q,B)) * (IncProj (A,a,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
and
A5:
not A,B,C are_concurrent
and
A6:
B,C,Q are_concurrent
and
A7:
not a on Q
and
A8:
( B <> Q & a <> b & a on O & b on O )
; ex q being POINT of IPP st
( q on O & not q on B & not q on Q & (IncProj (C,b,B)) * (IncProj (A,a,C)) = (IncProj (Q,q,B)) * (IncProj (A,a,Q)) )
A9:
( IncProj (B,b,C) is one-to-one & IncProj (C,a,A) is one-to-one )
by A1, A2, A3, A4, Th7;
not B,A,C are_concurrent
by A5;
then consider q being POINT of IPP such that
A10:
q on O
and
A11:
( not q on B & not q on Q )
and
A12:
(IncProj (C,a,A)) * (IncProj (B,b,C)) = (IncProj (Q,a,A)) * (IncProj (B,q,Q))
by A1, A2, A3, A4, A6, A7, A8, Th20;
take
q
; ( q on O & not q on B & not q on Q & (IncProj (C,b,B)) * (IncProj (A,a,C)) = (IncProj (Q,q,B)) * (IncProj (A,a,Q)) )
thus
( q on O & not q on B & not q on Q )
by A10, A11; (IncProj (C,b,B)) * (IncProj (A,a,C)) = (IncProj (Q,q,B)) * (IncProj (A,a,Q))
A13:
IncProj (B,q,Q) is one-to-one
by A11, Th7;
A14:
IncProj (Q,a,A) is one-to-one
by A1, A7, Th7;
thus (IncProj (C,b,B)) * (IncProj (A,a,C)) =
((IncProj (B,b,C)) ") * (IncProj (A,a,C))
by A2, A4, Th8
.=
((IncProj (B,b,C)) ") * ((IncProj (C,a,A)) ")
by A1, A3, Th8
.=
((IncProj (Q,a,A)) * (IncProj (B,q,Q))) "
by A12, A9, FUNCT_1:44
.=
((IncProj (B,q,Q)) ") * ((IncProj (Q,a,A)) ")
by A13, A14, FUNCT_1:44
.=
(IncProj (Q,q,B)) * ((IncProj (Q,a,A)) ")
by A11, Th8
.=
(IncProj (Q,q,B)) * (IncProj (A,a,Q))
by A1, A7, Th8
; verum