:: deftheorem Def01 defines BK_to_REAL2 BKMODEL2:def 2 :
for P being Element of BK_model
for b₂ being Element of inside_of_circle (0,0,1) holds
( b₂ = BK_to_REAL2 P iff ex u being non zero Element of (TOP-REAL 3) st
( Dir u = P & u . 3 = 1 & b₂ = |[(u . 1),(u . 2)]| ) );