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 A1, TARSKI:def 3;
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 A4, TARSKI:def 1; :: thesis: verum

end;

hence A = {g} by SUBSET_1:3; :: thesis: verum

end;