|.(|[a,b]| - |[a,b]|).| = 0 by TOPRNS_1:28;
hence not closed_inside_of_circle (a,b,r) is empty by Th42; :: thesis: verum