let G be IncProjectivePlane; 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; 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; ( 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
; ( m * e <> m9 * e & e * m <> e * m9 )
set L1 = m * e;
set L2 = m9 * e;
A5:
now 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
;
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;
verum end;
hence
( m * e <> m9 * e & e * m <> e * m9 )
by A5; verum