theorem Th20: :: PROJRED1:20

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