let a, b, r be Real; (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:8;
A1:
cl_Ball (p,r) = closed_inside_of_circle (a,b,r)
by Th45;
( Sphere (p,r) = circle (a,b,r) & Ball (p,r) = inside_of_circle (a,b,r) )
by Th46, Th47;
hence
(inside_of_circle (a,b,r)) \/ (circle (a,b,r)) = closed_inside_of_circle (a,b,r)
by A1, METRIC_1:16; verum