for P, Q being non point_at_infty Element of (ProjectiveSpace (TOP-REAL 3)) st RP3_to_T2 P = RP3_to_T2 Q holds
P = Q