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