let T be non empty Reflexive symmetric triangle MetrStruct ; :: thesis: ( T is totally_bounded implies T is bounded )

assume T is totally_bounded ; :: thesis: T is bounded

then consider Y being Subset-Family of T such that

A1: ( Y is finite & the carrier of T = union Y ) and

A2: for P being Subset of T st P in Y holds

ex x being Element of T st P = Ball (x,1) ;

for P being Subset of T st P in Y holds

P is bounded

hence T is bounded by Th18; :: thesis: verum

assume T is totally_bounded ; :: thesis: T is bounded

then consider Y being Subset-Family of T such that

A1: ( Y is finite & the carrier of T = union Y ) and

A2: for P being Subset of T st P in Y holds

ex x being Element of T st P = Ball (x,1) ;

for P being Subset of T st P in Y holds

P is bounded

proof

then
[#] T is bounded
by A1, Th17;
let P be Subset of T; :: thesis: ( P in Y implies P is bounded )

assume P in Y ; :: thesis: P is bounded

then ex x being Element of T st P = Ball (x,1) by A2;

hence P is bounded ; :: thesis: verum

end;assume P in Y ; :: thesis: P is bounded

then ex x being Element of T st P = Ball (x,1) by A2;

hence P is bounded ; :: thesis: verum

hence T is bounded by Th18; :: thesis: verum