let a, b, r be real number ; :: thesis: (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: Sphere p,r = circle a,b,r by Th49;
A2: Ball p,r = inside_of_circle a,b,r by Th48;
cl_Ball p,r = closed_inside_of_circle a,b,r by Th47;
hence (inside_of_circle a,b,r) \/ (circle a,b,r) = closed_inside_of_circle a,b,r by A1, A2, METRIC_1:17; :: thesis: verum