for P being non point_at_infty Element of (ProjectiveSpace (TOP-REAL 3)) st P in absolute holds
RP3_to_REAL2 P in circle (0,0,1)