for P being POINT of TarskiEuclid2Space st Tn2TR P is Element of inside_of_circle (0,0,1) holds
BK_to_T2 (T2_to_BK P) = P