let G be IncProjectivePlane; :: thesis: for e, m, m9 being POINT of G

for I being LINE of G st m on I & m9 on I & m <> m9 & e |' I holds

( m * e <> m9 * e & e * m <> e * m9 )

let e, m, m9 be POINT of G; :: thesis: for I being LINE of G st m on I & m9 on I & m <> m9 & e |' I holds

( m * e <> m9 * e & e * m <> e * m9 )

let I be LINE of G; :: thesis: ( m on I & m9 on I & m <> m9 & e |' I implies ( m * e <> m9 * e & e * m <> e * m9 ) )

assume that

A1: m on I and

A2: m9 on I and

A3: m <> m9 and

A4: e |' I ; :: thesis: ( m * e <> m9 * e & e * m <> e * m9 )

set L1 = m * e;

set L2 = m9 * e;

for I being LINE of G st m on I & m9 on I & m <> m9 & e |' I holds

( m * e <> m9 * e & e * m <> e * m9 )

let e, m, m9 be POINT of G; :: thesis: for I being LINE of G st m on I & m9 on I & m <> m9 & e |' I holds

( m * e <> m9 * e & e * m <> e * m9 )

let I be LINE of G; :: thesis: ( m on I & m9 on I & m <> m9 & e |' I implies ( m * e <> m9 * e & e * m <> e * m9 ) )

assume that

A1: m on I and

A2: m9 on I and

A3: m <> m9 and

A4: e |' I ; :: thesis: ( m * e <> m9 * e & e * m <> e * m9 )

set L1 = m * e;

set L2 = m9 * e;

A5: now :: thesis: not m * e = m9 * e

m on m * e
by A1, A4, Th16;

then A6: m on I,m * e by A1;

e on m * e by A1, A4, Th16;

then A7: m = I * (m * e) by A4, A6, Def9;

assume A8: m * e = m9 * e ; :: thesis: contradiction

m9 on m9 * e by A2, A4, Th16;

then A9: m9 on I,m9 * e by A2;

e on m9 * e by A2, A4, Th16;

hence contradiction by A3, A4, A8, A9, A7, Def9; :: thesis: verum

end;then A6: m on I,m * e by A1;

e on m * e by A1, A4, Th16;

then A7: m = I * (m * e) by A4, A6, Def9;

assume A8: m * e = m9 * e ; :: thesis: contradiction

m9 on m9 * e by A2, A4, Th16;

then A9: m9 on I,m9 * e by A2;

e on m9 * e by A2, A4, Th16;

hence contradiction by A3, A4, A8, A9, A7, Def9; :: thesis: verum

now :: thesis: not e * m = e * m9

hence
( m * e <> m9 * e & e * m <> e * m9 )
by A5; :: thesis: verumassume A10:
e * m = e * m9
; :: thesis: contradiction

m * e = e * m by A1, A4, Th16;

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

end;m * e = e * m by A1, A4, Th16;

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