:: deftheorem defines RP3_to_T2 BKMODEL4:def 6 :
for P being non point_at_infty Point of (ProjectiveSpace (TOP-REAL 3)) holds RP3_to_T2 P = RP3_to_REAL2 P;