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;

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;

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

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

hence ( m * e <> m9 * e & e * m <> e * m9 ) by A5; :: thesis: verum