CircleMap . (R^1 0) = c[10] by Th33;
hence Circle2IntervalR is open by Th43, TOPREALA:34; :: thesis: verum