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