let G be IncProjSp; :: thesis: for a, b, c being POINT of G st c on a * b & a <> c holds
b on a * c
let a, b, c be POINT of G; :: thesis: ( c on a * b & a <> c implies b on a * c )
assume A1: ( c on a * b & a <> c ) ; :: thesis: b on a * c

now

assume A2: a <> b ; :: thesis: b on a * c
then ( a on a * b & a on a * c & c on a * c ) by A1, Th16;
then a * b = a * c by A1, INCPROJ:def 9;
hence b on a * c by A2, Th16; :: thesis: verum

end;

hence b on a * c by A1, Th16; :: thesis: verum