let G be IncProjectivePlane; for e being POINT of G
for I, L1, L2 being LINE of G st e on L1 & e on L2 & L1 <> L2 & e |' I holds
( I * L1 <> I * L2 & L1 * I <> L2 * I )
let e be POINT of G; for I, L1, L2 being LINE of G st e on L1 & e on L2 & L1 <> L2 & e |' I holds
( I * L1 <> I * L2 & L1 * I <> L2 * I )
let I, L1, L2 be LINE of G; ( e on L1 & e on L2 & L1 <> L2 & e |' I implies ( I * L1 <> I * L2 & L1 * I <> L2 * I ) )
assume that
A1:
e on L1
and
A2:
e on L2
and
A3:
L1 <> L2
and
A4:
e |' I
; ( I * L1 <> I * L2 & L1 * I <> L2 * I )
set p1 = I * L1;
set p2 = I * L2;
A5:
now not I * L1 = I * L2
I * L1 on L1
by A1, A4, Th24;
then A6:
{e,(I * L1)} on L1
by A1, INCSP_1:1;
I * L1 on I
by A1, A4, Th24;
then A7:
L1 = e * (I * L1)
by A4, A6, Def8;
assume A8:
I * L1 = I * L2
;
contradiction
I * L2 on L2
by A2, A4, Th24;
then A9:
{e,(I * L2)} on L2
by A2, INCSP_1:1;
I * L2 on I
by A2, A4, Th24;
hence
contradiction
by A3, A4, A8, A9, A7, Def8;
verum end;
hence
( I * L1 <> I * L2 & L1 * I <> L2 * I )
by A5; verum