:: deftheorem Def1 defines IncProj PROJRED1:def 1 :
for IPP being 2-dimensional Desarguesian IncProjSp
for K, L being LINE of IPP
for p being POINT of IPP st not p on K & not p on L holds
for b₅ being PartFunc of the Points of IPP, the Points of IPP holds
( b₅ = IncProj (K,p,L) iff ( dom b₅ c= the Points of IPP & ( for x being POINT of IPP holds
( x in dom b₅ iff x on K ) ) & ( for x, y being POINT of IPP st x on K & y on L holds
( b₅ . x = y iff ex X being LINE of IPP st
( p on X & x on X & y on X ) ) ) ) );