:: deftheorem Def02 defines T2_to_BK BKMODEL4:def 2 :
for P being POINT of TarskiEuclid2Space st Tn2TR P in inside_of_circle (0,0,1) holds
for b₂ being POINT of BK-model-Plane holds
( b₂ = T2_to_BK P iff ex u being non zero Element of (TOP-REAL 3) st
( b₂ = Dir u & u `3 = 1 & Tn2TR P = |[(u `1),(u `2)]| ) );