for P, Q, P1 being non point_at_infty Element of (ProjectiveSpace (TOP-REAL 3)) st P in BK_model & Q in BK_model & P1 in absolute holds
not between RP3_to_T2 Q, RP3_to_T2 P1, RP3_to_T2 P