:: deftheorem Def14 defines Circle2IntervalL TOPREALB:def 14 :
for b₁ being Function of (Topen_unit_circle c[-10]),(R^1 | (R^1 ].(1 / 2),(3 / 2).[)) holds
( b₁ = Circle2IntervalL iff for p being Point of (Topen_unit_circle c[-10]) ex x, y being Real st
( p = |[x,y]| & ( y >= 0 implies b₁ . p = 1 + ((arccos x) / (2 * PI)) ) & ( y <= 0 implies b₁ . p = 1 - ((arccos x) / (2 * PI)) ) ) );