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