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

let A be Subset of M; :: thesis: ( A <> {} & A is bounded & diameter A = 0 implies ex g being Point of M st A = {g} )
assume that
A1: A <> {} and
A2: A is bounded ; :: thesis: ( not diameter A = 0 or ex g being Point of M st A = {g} )
thus ( diameter A = 0 implies ex g being Point of M st A = {g} ) :: thesis: verum
proof
set g = the Element of A;
reconsider g = the Element of A as Element of M by ;
assume A3: diameter A = 0 ; :: thesis: ex g being Point of M st A = {g}
reconsider Z = {g} as Subset of M ;
take g ; :: thesis: A = {g}
for x being Element of M holds
( x in A iff x in Z )
proof
let x be Element of M; :: thesis: ( x in A iff x in Z )
thus ( x in A implies x in Z ) :: thesis: ( x in Z implies x in A )
proof
assume x in A ; :: thesis: x in Z
then dist (x,g) <= 0 by A2, A3, Def8;
then dist (x,g) = 0 by METRIC_1:5;
then x = g by METRIC_1:2;
hence x in Z by TARSKI:def 1; :: thesis: verum
end;
assume A4: x in Z ; :: thesis: x in A
g in A by A1;
hence x in A by ; :: thesis: verum
end;
hence A = {g} by SUBSET_1:3; :: thesis: verum
end;