:: deftheorem Def01 defines BK_to_T2 BKMODEL4:def 1 :
for P being POINT of BK-model-Plane
for b₂ being POINT of TarskiEuclid2Space holds
( b₂ = BK_to_T2 P iff ex p being Element of BK_model st
( P = p & b₂ = BK_to_REAL2 p ) );