let a, b, r be real number ; (inside_of_circle (a,b,r)) \/ (circle (a,b,r)) = closed_inside_of_circle (a,b,r)
reconsider p = |[a,b]| as Point of (Euclid 2) by TOPREAL3:13;
A1:
cl_Ball (p,r) = closed_inside_of_circle (a,b,r)
by Th47;
( Sphere (p,r) = circle (a,b,r) & Ball (p,r) = inside_of_circle (a,b,r) )
by Th48, Th49;
hence
(inside_of_circle (a,b,r)) \/ (circle (a,b,r)) = closed_inside_of_circle (a,b,r)
by A1, METRIC_1:17; verum