theorem Th14: :: PROJRED2:14

for IPP being 2-dimensional Desarguesian IncProjSp
for a, b, c, d, p, pp9, q being POINT of IPP
for O1, O2, O3, 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 & c on A & c on C & c on Q & not b on Q & A <> Q & a on O & b on O & not B,C,O are_concurrent & d on C & d on B & a on O1 & d on O1 & p on A & p on O1 & q on O & q on O2 & p on O2 & pp9 on O2 & d on O3 & b on O3 & pp9 on O3 & pp9 on Q & q <> a & not q on A & not q on Q holds
(IncProj (C,b,B)) * (IncProj (A,a,C)) = (IncProj (Q,b,B)) * (IncProj (A,q,Q))