:: deftheorem defines REAL2_to_absolute BKMODEL1:def 9 :
for u being non zero Element of (TOP-REAL 2) st u in circle (0,0,1) holds
REAL2_to_absolute u = Dir |[(u . 1),(u . 2),1]|;