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 that

A1: r1 <> r2 and

A2: r1 on H and

A3: r2 on H and

A4: q1 |' H and

A5: q2 |' H and

A6: q1 * r1 = q2 * r2 ; :: thesis: contradiction

set L1 = q1 * r1;

set L2 = q2 * r2;

A7: q1 on q1 * r1 by A2, A4, Th16;

r2 on q2 * r2 by A3, A5, Th16;

then A8: r2 on q2 * r2,H by A3;

r1 on q1 * r1 by A2, A4, Th16;

then r1 on q1 * r1,H by A2;

then r1 = (q1 * r1) * H by A4, A7, Def9;

hence contradiction by A1, A4, A6, A7, A8, Def9; :: thesis: verum

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 that

A1: r1 <> r2 and

A2: r1 on H and

A3: r2 on H and

A4: q1 |' H and

A5: q2 |' H and

A6: q1 * r1 = q2 * r2 ; :: thesis: contradiction

set L1 = q1 * r1;

set L2 = q2 * r2;

A7: q1 on q1 * r1 by A2, A4, Th16;

r2 on q2 * r2 by A3, A5, Th16;

then A8: r2 on q2 * r2,H by A3;

r1 on q1 * r1 by A2, A4, Th16;

then r1 on q1 * r1,H by A2;

then r1 = (q1 * r1) * H by A4, A7, Def9;

hence contradiction by A1, A4, A6, A7, A8, Def9; :: thesis: verum