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

( 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