for IPP being IncProjSp
for a, b being POINT of IPP st a <> b holds
ex A, B being LINE of IPP st
( a on A & not a on B & b on B & not b on A )