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