theorem :: PROJRED2:22

for IPP being 2-dimensional Desarguesian IncProjSp
for a, b, c, d, r, s being POINT of IPP
for A, B, C, Q, R, S being LINE of IPP st not a on A & not b on B & not a on C & not b on C & not a on B & not b on A & c on A & c on C & d on B & d on C & a on S & d on S & c on R & b on R & s on A & s on S & r on B & r on R & s on Q & r on Q & not A,B,C are_concurrent holds
(IncProj (C,b,B)) * (IncProj (A,a,C)) = (IncProj (Q,a,B)) * (IncProj (A,b,Q))