for IPP being IncProjSp
for a being POINT of IPP holds
not for A being LINE of IPP holds a on A