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

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 )

hence
b on a * c
by A2, Th16; :: thesis: verumassume 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;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