let G be IncProjectivePlane; :: thesis: 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; :: thesis: ( 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 ) ; :: thesis: a on c * d
a * c = c * d by A1, A2, A3, Th28;
hence a on c * d by A2, Th16; :: thesis: verum