closed_inside_of_circle (a,b,r) = { q where q is Point of (TOP-REAL 2) : |.(q - |[a,b]|).| <= r } by JGRAPH_6:def 7;
hence closed_inside_of_circle (a,b,r) is convex by Lm1; :: thesis: verum