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