let M be non empty MetrSpace; :: thesis: for S being non empty Subset of M
for T being non empty Subset of (TopSpaceMetr M) st T = S holds
( (TopSpaceMetr M) | T is countably_compact iff S is sequentially_compact )
let S be non empty Subset of M; :: thesis: for T being non empty Subset of (TopSpaceMetr M) st T = S holds
( (TopSpaceMetr M) | T is countably_compact iff S is sequentially_compact )
let T be non empty Subset of (TopSpaceMetr M); :: thesis: ( T = S implies ( (TopSpaceMetr M) | T is countably_compact iff S is sequentially_compact ) )
assume A1: T = S ; :: thesis: ( (TopSpaceMetr M) | T is countably_compact iff S is sequentially_compact )

hereby :: thesis: ( S is sequentially_compact implies (TopSpaceMetr M) | T is countably_compact )

assume (TopSpaceMetr M) | T is countably_compact ; :: thesis: S is sequentially_compact
then TopSpaceMetr (M | S) is countably_compact by A1, HAUSDORF:16;
then M | S is sequentially_compact by Th11, COMPL_SP:35;
hence S is sequentially_compact by Th14; :: thesis: verum

end;

assume S is sequentially_compact ; :: thesis: (TopSpaceMetr M) | T is countably_compact
then M | S is sequentially_compact by Th14;
then TopSpaceMetr (M | S) is countably_compact by Th11, COMPL_SP:35;
hence (TopSpaceMetr M) | T is countably_compact by A1, HAUSDORF:16; :: thesis: verum