let G be IncProjectivePlane; :: thesis: for a, b, c being POINT of G holds
( not a on b * c or b = a or b = c or c on b * a )
let a, b, c be POINT of G; :: thesis: ( not a on b * c or b = a or b = c or c on b * a )
assume that
A1: ( a on b * c & b <> a ) and
A2: b <> c ; :: thesis: c on b * a
b * c = c * b by A2, Th16;
hence c on b * a by A1, A2, Th35; :: thesis: verum