theorem :: PROJRED2:21

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