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 A1: ( e on L1 & e on L2 & L1 <> L2 & e |' I ) ; :: thesis: ( I * L1 <> I * L2 & L1 * I <> L2 * I )
set p1 = I * L1;
set p2 = I * L2;

A2: now

assume A3: I * L1 = I * L2 ; :: thesis: contradiction
A4: ( I * L1 on I & I * L2 on I & I * L1 on L1 & I * L2 on L2 ) by A1, Th24;
then ( {e,(I * L1)} on L1 & {e,(I * L2)} on L2 ) by A1, INCSP_1:11;
then ( L1 = e * (I * L1) & L2 = e * (I * L2) ) by A1, A4, Def8;
hence contradiction by A1, A3; :: thesis: verum

end;

now

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

end;

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