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