theorem :: PROJPL_1:30

for G being 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 )