let r be real number ; :: 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

assume r = 0 ; :: thesis: contradiction
then A4: cl_Ball z3,r = {z3} by TOPREAL6:64;
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:63; :: thesis: verum