let G be IncProjectivePlane; :: thesis: for q1, q2, r1, r2 being POINT of G
for H being LINE of G st r1 <> r2 & r1 on H & r2 on H & q1 |' H & q2 |' H holds
q1 * r1 <> q2 * r2
let q1, q2, r1, r2 be POINT of G; :: thesis: for H being LINE of G st r1 <> r2 & r1 on H & r2 on H & q1 |' H & q2 |' H holds
q1 * r1 <> q2 * r2
let H be LINE of G; :: thesis: ( r1 <> r2 & r1 on H & r2 on H & q1 |' H & q2 |' H implies q1 * r1 <> q2 * r2 )
assume A1: ( r1 <> r2 & r1 on H & r2 on H & q1 |' H & q2 |' H & q1 * r1 = q2 * r2 ) ; :: thesis: contradiction
set L1 = q1 * r1;
set L2 = q2 * r2;
A2: ( q1 on q1 * r1 & q2 on q2 * r2 & r1 on q1 * r1 & r2 on q2 * r2 ) by A1, Th16;
then ( r1 on q1 * r1,H & r2 on q2 * r2,H ) by A1, Def2;
then ( r1 = (q1 * r1) * H & r2 = (q2 * r2) * H ) by A1, A2, Def9;
hence contradiction by A1; :: thesis: verum