let P be POINT of BK-model-Plane; :: thesis: Tn2TR (BK_to_T2 P) in inside_of_circle (0,0,1)
consider p being Element of BK_model such that
P = p and
A1: BK_to_T2 P = BK_to_REAL2 p by Def01;
reconsider Q = BK_to_T2 P as POINT of TarskiEuclid2Space ;
thus Tn2TR (BK_to_T2 P) in inside_of_circle (0,0,1) by A1; :: thesis: verum