:: deftheorem Def3 defines Projection PROJRED2:def 3 :
for IPP being 2-dimensional Desarguesian IncProjSp
for b₂ being PartFunc of the Points of IPP, the Points of IPP holds
( b₂ is Projection of IPP iff ex a being POINT of IPP ex A, B being LINE of IPP st
( not a on A & not a on B & b₂ = IncProj (A,a,B) ) );