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