let G be IncProjectivePlane; :: thesis: for a, b, c being POINT of G holds

( not a on b * c or a = c or b = c or b on c * a )

let a, b, c be POINT of G; :: thesis: ( not a on b * c or a = c or b = c or b on c * a )

assume that

A1: a on b * c and

A2: a <> c and

A3: b <> c ; :: thesis: b on c * a

c on b * c by A3, Th16;

then A4: {c,a} on b * c by A1, INCSP_1:1;

b on b * c by A3, Th16;

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

( not a on b * c or a = c or b = c or b on c * a )

let a, b, c be POINT of G; :: thesis: ( not a on b * c or a = c or b = c or b on c * a )

assume that

A1: a on b * c and

A2: a <> c and

A3: b <> c ; :: thesis: b on c * a

c on b * c by A3, Th16;

then A4: {c,a} on b * c by A1, INCSP_1:1;

b on b * c by A3, Th16;

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