for P being Point of (ProjectiveSpace (TOP-REAL 3)) st ex u being non zero Element of (TOP-REAL 3) st
( P = Dir u & u `3 <> 0 ) holds
not P is point_at_infty