theorem :: TOPREAL9:55

for a, b, r being Real holds (inside_of_circle (a,b,r)) \/ (circle (a,b,r)) = closed_inside_of_circle (a,b,r)