let G be IncProjectivePlane; 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; ( 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
; 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; verum