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