theorem :: PROJRED1:21

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