theorem Th24: :: PROJRED1:24

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