:: deftheorem defines closed_inside_of_circle JGRAPH_6:def 7 :
for a, b, r being Real holds closed_inside_of_circle (a,b,r) = { p where p is Point of (TOP-REAL 2) : |.(p - |[a,b]|).| <= r } ;