reconsider r = 0 as Integer ;
CircleMap (R^1 ((1 / 2) + r)) is open ;
hence CircleMap (R^1 (1 / 2)) is being_homeomorphism by TOPREALA:16; :: thesis: verum