:: deftheorem Def1 defines sequentially_compact TOPMETR4:def 1 :
for M being non empty MetrSpace
for X being Subset of M holds
( X is sequentially_compact iff for S1 being sequence of M st rng S1 c= X holds
ex S2 being sequence of M st
( ex N being increasing sequence of NAT st S2 = S1 * N & S2 is convergent & lim S2 in X ) );