for P being non point_at_infty Point of (ProjectiveSpace (TOP-REAL 3))
for Q being Element of BK_model st P = Q holds
RP3_to_REAL2 P = BK_to_REAL2 Q