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

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 )

end;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

hence
A = {g}
by SUBSET_1:3; :: thesis: verum
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 )

g in A by A1;

hence x in A by A4, TARSKI:def 1; :: thesis: verum

end;thus ( x in A implies x in Z ) :: thesis: ( x in Z implies x in A )

proof

assume A4:
x in Z
; :: thesis: x in A
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;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

g in A by A1;

hence x in A by A4, TARSKI:def 1; :: thesis: verum