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 that
A1: c on a * b and
A2: a <> c ; :: thesis: b on a * c

now :: thesis: ( a <> b implies b on a * c )

assume A3: a <> b ; :: thesis: b on a * c
then a on a * b by Th16;
then a * b = a * c by A1, A2, Th16;
hence b on a * c by A3, Th16; :: thesis: verum

end;

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