for P being POINT of BK-model-Plane holds Tn2TR (BK_to_T2 P) in inside_of_circle (0,0,1)