let M be non empty MetrSpace; :: thesis: for S being non empty Subset of M holds
( S is sequentially_compact iff M | S is compact )
let S be non empty Subset of M; :: thesis: ( S is sequentially_compact iff M | S is compact )
( M | S is sequentially_compact iff M | S is compact ) by Th11;
hence ( S is sequentially_compact iff M | S is compact ) by Th14; :: thesis: verum