for IPP being IncProjSp
for a, b, c, o being POINT of IPP
for A, B, P, Q being LINE of IPP st o on A & o on B & A <> B & a on A & o <> a & b on B & c on B & b <> c & a on P & b on P & c on Q holds
P <> Q