theorem Th63: :: BKMODEL4:73

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