for IPP being IncProjSp
for A being LINE of IPP ex a being POINT of IPP st a on A