let M be non empty MetrSpace; :: thesis: for S being non empty Subset of M holds
( ( M | S is totally_bounded & M | S is complete ) iff S is sequentially_compact )
let S be non empty Subset of M; :: thesis: ( ( M | S is totally_bounded & M | S is complete ) iff S is sequentially_compact )

hereby :: thesis: ( S is sequentially_compact implies ( M | S is totally_bounded & M | S is complete ) )

assume ( M | S is totally_bounded & M | S is complete ) ; :: thesis: S is sequentially_compact
then M | S is sequentially_compact by Th12;
hence S is sequentially_compact by Th14; :: thesis: verum

end;

assume S is sequentially_compact ; :: thesis: ( M | S is totally_bounded & M | S is complete )
then M | S is sequentially_compact by Th14;
hence ( M | S is totally_bounded & M | S is complete ) by Th12; :: thesis: verum