theorem :: PROJRED2:12

for IPP being 2-dimensional Desarguesian IncProjSp
for o being POINT of IPP
for A, B, C being LINE of IPP st not o on A & not o on B & not o on C holds
(IncProj (C,o,B)) * (IncProj (A,o,C)) = IncProj (A,o,B)