theorem :: TOPREAL9:46

for a, b, r being Real holds circle (a,b,r) c= closed_inside_of_circle (a,b,r)