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