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: 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; :: thesis: verum