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 A1: ( A <> {} & 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

assume A2: diameter A = 0 ; :: thesis: ex g being Point of M st A = {g}
consider g being Element of A;
reconsider g = g as Element of M by A1, TARSKI:def 3;
take g ; :: thesis: A = {g}
reconsider Z = {g} as Subset of M ;
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 A1, A2, Def10;
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;

A3: g in A by A1;
assume x in Z ; :: thesis: x in A
hence x in A by A3, TARSKI:def 1; :: thesis: verum

end;

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

end;