for R1, R2 being Point of TarskiEuclid2Space st Tn2TR R1 in circle (0,0,1) & Tn2TR R2 in circle (0,0,1) & R1 <> R2 holds
ex P being Element of BK-model-Plane st between R1, BK_to_T2 P,R2