for P being Element of absolute holds P is non point_at_infty Element of (ProjectiveSpace (TOP-REAL 3))