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;

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;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

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

hence
( I * L1 <> I * L2 & L1 * I <> L2 * I )
by A5; :: thesis: verumassume 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;L1 * I = I * L1 by A1, A4, Th24;

hence contradiction by A2, A4, A5, A10, Th24; :: thesis: verum