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

A2: now

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

end;

now

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

end;

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