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

per cases ( T0 = {} or T0 <> {} ) ;

suppose T0 = {} ; :: thesis: ( T0 is compact iff S0 is sequentially_compact )

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

end;

suppose A2: T0 <> {} ; :: thesis: ( T0 is compact iff S0 is sequentially_compact )

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

hereby :: thesis: ( S0 is sequentially_compact implies T0 is compact )

assume T0 is compact ; :: thesis: S0 is sequentially_compact
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: verum

end;

assume S0 is sequentially_compact ; :: thesis: T0 is compact
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: verum

end;

end;