let G be IncProjectivePlane; 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; 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; ( 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
; 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; verum