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