theorem :: PROJPL_1:33

for G being IncProjSp
for a, b, c being POINT of G st c on a * b & a <> c holds
b on a * c