:: deftheorem Def02 defines REAL2_to_BK BKMODEL2:def 3 :
for Q being Element of inside_of_circle (0,0,1)
for b₂ being Element of BK_model holds
( b₂ = REAL2_to_BK Q iff ex P being Element of (TOP-REAL 2) st
( P = Q & b₂ = Dir |[(P `1),(P `2),1]| ) );