theorem
for
IPP being
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)) )