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 * c = 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 * c = c * d )

assume that

A1: ( a * c = b * d & not a = c & not b = d ) and

A2: not c = d ; :: thesis: a * c = c * d

( c on a * c & d on a * c ) by A1, Th16;

hence a * c = c * d by A2, Th16; :: thesis: verum

( not a * c = b * d or a = c or b = d or c = d or a * c = 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 * c = c * d )

assume that

A1: ( a * c = b * d & not a = c & not b = d ) and

A2: not c = d ; :: thesis: a * c = c * d

( c on a * c & d on a * c ) by A1, Th16;

hence a * c = c * d by A2, Th16; :: thesis: verum