:: deftheorem defines absolute_to_REAL2 BKMODEL1:def 8 :
for P being Element of absolute
for b₂ being Element of circle (0,0,1) holds
( b₂ = absolute_to_REAL2 P iff ex u being non zero Element of (TOP-REAL 3) st
( P = Dir u & u . 3 = 1 & b₂ = |[(u . 1),(u . 2)]| ) );