theorem :: TOPREAL9:51

for a, b, r being Real holds cl_Ball (|[a,b]|,r) = closed_inside_of_circle (a,b,r)