let a, b, r be real number ; :: thesis: circle a,b,r c= closed_inside_of_circle a,b,r
let x be set ; :: 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, Th43;
hence x in closed_inside_of_circle a,b,r by Th44; :: thesis: verum