:: deftheorem Def13 defines Circle2IntervalR TOPREALB:def 13 :
for b₁ being Function of (Topen_unit_circle c[10]),(R^1 | (R^1 ].0,1.[)) holds
( b₁ = Circle2IntervalR 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 = (arccos x) / (2 * PI) ) & ( y <= 0 implies b₁ . p = 1 - ((arccos x) / (2 * PI)) ) ) );