for l being Element of ProjectiveLines real_projective_plane holds dual (dual l) = l