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