for P being Point of real_projective_plane holds not P in dual P