theorem :: TBSP_1:22

for M being non empty MetrSpace
for A being Subset of M st A <> {} & A is bounded & diameter A = 0 holds
ex g being Point of M st A = {g}