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 A1: ( a * c = b * d & not a = c & not b = d & not c = d ) ; :: thesis: a * c = c * d
then ( c on a * c & d on a * c & c on c * d & d on c * d ) by Th16;
hence a * c = c * d by A1, INCPROJ:def 9; :: thesis: verum