let a, b, r be Real; :: thesis: circle (a,b,r) c= closed_inside_of_circle (a,b,r)
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in circle (a,b,r) or x in closed_inside_of_circle (a,b,r) )
assume A1: x in circle (a,b,r) ; :: thesis: x in closed_inside_of_circle (a,b,r)
then reconsider x = x as Point of (TOP-REAL 2) ;
|.(x - |[a,b]|).| = r by A1, Th41;
hence x in closed_inside_of_circle (a,b,r) by Th42; :: thesis: verum