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

( 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