CircleMap . (R^1 0) = c[10] by Th32;
hence CircleMap (R^1 0) is open by Th42, TOPREALA:14; :: thesis: verum