let M be non empty MetrSpace; :: thesis:
let S0 be Subset of M; :: thesis:
let T0 be Subset of (TopSpaceMetr M); :: thesis:
assume A1: T0 = S0 ; :: thesis:

suppose T0 = {} ; :: thesis:

hence ( T0 is compact iff S0 is sequentially_compact ) by A1; :: thesis:

end;

suppose A2: T0 <> {} ; :: thesis:

then reconsider T = T0 as non empty Subset of (TopSpaceMetr M) ;
reconsider S = T0 as non empty Subset of M by A2;

hereby :: thesis:

assume T0 is compact ; :: thesis:
then (TopSpaceMetr M) | T is compact ;
then TopSpaceMetr (M | S) is compact by HAUSDORF:16;
then M | S is sequentially_compact by Th11;
hence S0 is sequentially_compact by A1, Th14; :: thesis:

end;

assume S0 is sequentially_compact ; :: thesis:
then M | S is sequentially_compact by A1, Th14;
then TopSpaceMetr (M | S) is compact by Th11;
then (TopSpaceMetr M) | T is compact by HAUSDORF:16;
hence T0 is compact by COMPTS_1:3; :: thesis:

end;

end;