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 A1: ( a on b * c & b <> a & b <> c ) ; :: thesis: c on b * a
then b * c = c * b by Th16;
hence c on b * a by A1, Th35; :: thesis: verum