for R1, R2 being non point_at_infty Element of (ProjectiveSpace (TOP-REAL 3)) st R1 in absolute & R2 in absolute & R1 <> R2 holds
ex P being Element of BK-model-Plane st between RP3_to_T2 R1, BK_to_T2 P, RP3_to_T2 R2