let G be IncProjectivePlane; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ; :: thesis: ( I * L1 <> I * L2 & L1 * I <> L2 * I )
set p1 = I * L1;
set p2 = I * L2;

A5: now :: thesis: 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 ; :: thesis: 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; :: thesis: verum

end;

now :: thesis: not L1 * I = L2 * I

assume A10: L1 * I = L2 * I ; :: thesis: contradiction
L1 * I = I * L1 by A1, A4, Th24;
hence contradiction by A2, A4, A5, A10, Th24; :: thesis: verum

end;

hence ( I * L1 <> I * L2 & L1 * I <> L2 * I ) by A5; :: thesis: verum