let a, b, r be real number ; :: 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 set 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, Th43;
hence contradiction by A1, Th45; :: thesis: verum