for P, Q being Element of BK_model st P <> Q holds
ex R being Element of absolute st
for p, q, r being non point_at_infty Element of (ProjectiveSpace (TOP-REAL 3)) st p = P & q = Q & r = R holds
between RP3_to_T2 p, RP3_to_T2 q, RP3_to_T2 r