theorem :: TOPREAL9:54

for a, b, r being Real holds inside_of_circle (a,b,r) misses circle (a,b,r)