theorem Th18: :: PROJRED1:18

for IPP being 2-dimensional Desarguesian IncProjSp
for p being POINT of IPP
for K being LINE of IPP st not p on K holds
for x being POINT of IPP st x on K holds
(IncProj (K,p,K)) . x = x