theorem Th42: :: TOPREALB:42

(CircleMap (R^1 0)) " = Circle2IntervalR