let a, b, r be Real; :: thesis: for t being Point of (TOP-REAL 2) holds
( t in closed_inside_of_circle (a,b,r) iff |.(t - |[a,b]|).| <= r )
let t be Point of (TOP-REAL 2); :: thesis: ( t in closed_inside_of_circle (a,b,r) iff |.(t - |[a,b]|).| <= r )
A1: closed_inside_of_circle (a,b,r) = { x where x is Point of (TOP-REAL 2) : |.(x - |[a,b]|).| <= r } by JGRAPH_6:def 7;

hereby :: thesis: ( |.(t - |[a,b]|).| <= r implies t in closed_inside_of_circle (a,b,r) )

assume t in closed_inside_of_circle (a,b,r) ; :: thesis: |.(t - |[a,b]|).| <= r
then ex x being Point of (TOP-REAL 2) st
( t = x & |.(x - |[a,b]|).| <= r ) by A1;
hence |.(t - |[a,b]|).| <= r ; :: thesis: verum

end;

thus ( |.(t - |[a,b]|).| <= r implies t in closed_inside_of_circle (a,b,r) ) by A1; :: thesis: verum