let G be IncProjectivePlane; :: thesis: for e, m, m' being POINT of G
for I being LINE of G st m on I & m' on I & m <> m' & e |' I holds
( m * e <> m' * e & e * m <> e * m' )
let e, m, m' be POINT of G; :: thesis: for I being LINE of G st m on I & m' on I & m <> m' & e |' I holds
( m * e <> m' * e & e * m <> e * m' )
let I be LINE of G; :: thesis: ( m on I & m' on I & m <> m' & e |' I implies ( m * e <> m' * e & e * m <> e * m' ) )
assume that
A1: m on I and
A2: m' on I and
A3: m <> m' and
A4: e |' I ; :: thesis: ( m * e <> m' * e & e * m <> e * m' )
set L1 = m * e;
set L2 = m' * e;

A5: now

m on m * e by A1, A4, Th16;
then A6: m on I,m * e by A1, Def2;
e on m * e by A1, A4, Th16;
then A7: m = I * (m * e) by A4, A6, Def9;
assume A8: m * e = m' * e ; :: thesis: contradiction
m' on m' * e by A2, A4, Th16;
then A9: m' on I,m' * e by A2, Def2;
e on m' * e by A2, A4, Th16;
hence contradiction by A3, A4, A8, A9, A7, Def9; :: thesis: verum

end;

now

assume A10: e * m = e * m' ; :: thesis: contradiction
m * e = e * m by A1, A4, Th16;
hence contradiction by A2, A4, A5, A10, Th16; :: thesis: verum

end;

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