theorem :: TOPREAL7:24

for M, N being non empty MetrSpace st the carrier of M = the carrier of N & ( for m being Point of M
for n being Point of N
for r being Real st r > 0 & m = n holds
ex r1 being Real st
( r1 > 0 & Ball (n,r1) c= Ball (m,r) ) ) & ( for m being Point of M
for n being Point of N
for r being Real st r > 0 & m = n holds
ex r1 being Real st
( r1 > 0 & Ball (m,r1) c= Ball (n,r) ) ) holds
TopSpaceMetr M = TopSpaceMetr N