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

proof

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;

then [#] T is bounded by A1, Th17;
hence T is bounded by Th18; :: thesis: verum