let r be Real; for M being non empty MetrSpace
for z1, z2, z3 being Point of M st z1 <> z2 & z1 in cl_Ball (z3,r) & z2 in cl_Ball (z3,r) holds
r > 0
let M be non empty MetrSpace; for z1, z2, z3 being Point of M st z1 <> z2 & z1 in cl_Ball (z3,r) & z2 in cl_Ball (z3,r) holds
r > 0
let z1, z2, z3 be Point of M; ( z1 <> z2 & z1 in cl_Ball (z3,r) & z2 in cl_Ball (z3,r) implies r > 0 )
assume that
A1:
z1 <> z2
and
A2:
z1 in cl_Ball (z3,r)
and
A3:
z2 in cl_Ball (z3,r)
; r > 0
hence
r > 0
by A2, TOPREAL6:55; verum