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 and
A2: the carrier of T = union Y and
A3: for P being Subset of T st P in Y holds
ex x being Element of T st P = Ball x,1 by Def1;
for P being Subset of T st P in Y holds
P is bounded

proof

thus for P being Subset of T st P in Y holds
P is bounded :: thesis: verum

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 A3;
hence P is bounded by Th19; :: thesis: verum

end;

end;

then [#] T is bounded by A1, A2, Th24;
hence T is bounded by Th25; :: thesis: verum