let r be Real; :: thesis: 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; :: thesis: 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; :: thesis: ( 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) ; :: thesis: r > 0

now :: thesis: not r = 0

assume r = 0 ; :: thesis: contradiction
then A4: cl_Ball (z3,r) = {z3} by TOPREAL6:56;
then z1 = z3 by A2, TARSKI:def 1;
hence contradiction by A1, A3, A4, TARSKI:def 1; :: thesis: verum

end;

hence r > 0 by A2, TOPREAL6:55; :: thesis: verum