let a, b, r be Real; inside_of_circle (a,b,r) misses circle (a,b,r)
assume
not inside_of_circle (a,b,r) misses circle (a,b,r)
; 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; verum