for P being Point of BK-model-Plane
for p being Element of BK_model st P = p holds
( BK_to_T2 P = BK_to_REAL2 p & Tn2TR (BK_to_T2 P) = BK_to_REAL2 p )