for P being non zero_proj2 Point of (ProjectiveSpace (TOP-REAL 3))
for u being non zero Element of (TOP-REAL 3) st P = Dir u holds
u . 2 <> 0