theorem Th48: :: ANPROJ11:48

for l, m being Element of ProjectiveLines real_projective_plane holds
( l <> m iff dual l <> dual m )