for P, Q, R being Point of TarskiEuclid2Space st between P,Q,R & Tn2TR P in inside_of_circle (0,0,1) & Tn2TR R in inside_of_circle (0,0,1) holds
Tn2TR Q in inside_of_circle (0,0,1)