let a, b, r be Real; :: thesis: inside_of_circle (a,b,r) misses circle (a,b,r)
assume not inside_of_circle (a,b,r) misses circle (a,b,r) ; :: thesis: contradiction
then consider x being object such that
A1: x in inside_of_circle (a,b,r) and
A2: x in circle (a,b,r) by XBOOLE_0:3;
reconsider x = x as Point of (TOP-REAL 2) by A1;
|.(x - |[a,b]|).| = r by A2, Th41;
hence contradiction by A1, Th43; :: thesis: verum