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