let P, Q be Element of BK_model ; :: thesis: ( P <> Q implies 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 )
assume P <> Q ; :: thesis: 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
then consider R being Element of absolute such that
A1: for p, q, r being non point_at_infty Element of (ProjectiveSpace (TOP-REAL 3)) st p = Q & q = P & r = R holds
between RP3_to_T2 q, RP3_to_T2 p, RP3_to_T2 r by Th57;
take R ; :: thesis: 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
thus 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 by A1; :: thesis: verum