for P being Point of real_projective_plane
for l being Element of ProjectiveLines real_projective_plane st dual l in dual P holds
P in l