let Z be non empty MetrSpace; :: thesis: for H being non empty Subset of Z st Z is complete holds
( ( Z | H is totally_bounded implies Cl H is sequentially_compact ) & ( Cl H is sequentially_compact implies Z | H is totally_bounded ) & ( Z | H is totally_bounded implies Z | (Cl H) is compact ) & ( Z | (Cl H) is compact implies Z | H is totally_bounded ) )
let H be non empty Subset of Z; :: thesis: ( Z is complete implies ( ( Z | H is totally_bounded implies Cl H is sequentially_compact ) & ( Cl H is sequentially_compact implies Z | H is totally_bounded ) & ( Z | H is totally_bounded implies Z | (Cl H) is compact ) & ( Z | (Cl H) is compact implies Z | H is totally_bounded ) ) )
assume Z is complete ; :: thesis: ( ( Z | H is totally_bounded implies Cl H is sequentially_compact ) & ( Cl H is sequentially_compact implies Z | H is totally_bounded ) & ( Z | H is totally_bounded implies Z | (Cl H) is compact ) & ( Z | (Cl H) is compact implies Z | H is totally_bounded ) )
then Z | (Cl H) is complete by Th3;
hence ( Z | H is totally_bounded iff Cl H is sequentially_compact ) by TOPMETR4:17, Th4; :: thesis: ( Z | H is totally_bounded iff Z | (Cl H) is compact )
hence ( Z | H is totally_bounded iff Z | (Cl H) is compact ) by TOPMETR4:14; :: thesis: verum