for P being Element of absolute
for R being Element of real_projective_plane
for u being non zero Element of (TOP-REAL 3) st R in tangent P & R = Dir u & u . 3 = 0 holds
R = pole_infty P