theorem Th10: :: PROJRED2:10

for IPP being 2-dimensional Desarguesian IncProjSp
for o being POINT of IPP
for A being LINE of IPP st not o on A holds
IncProj (A,o,A) = id (CHAIN A)