let a, b, r be Real; :: thesis: for s, t being Point of (TOP-REAL 2) st s <> t & s in closed_inside_of_circle (a,b,r) & t in closed_inside_of_circle (a,b,r) holds
r > 0
let s, t be Point of (TOP-REAL 2); :: thesis: ( s <> t & s in closed_inside_of_circle (a,b,r) & t in closed_inside_of_circle (a,b,r) implies r > 0 )
reconsider x = |[a,b]| as Point of (Euclid 2) by TOPREAL3:8;
cl_Ball (x,r) = closed_inside_of_circle (a,b,r) by Th45;
hence ( s <> t & s in closed_inside_of_circle (a,b,r) & t in closed_inside_of_circle (a,b,r) implies r > 0 ) by Th4; :: thesis: verum