theorem :: TOPREAL9:53

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