let a, b, r be real number ; :: 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:13;
cl_Ball x,r = closed_inside_of_circle a,b,r by Th47;
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 Th6; :: thesis: verum