let M be non empty MetrSpace; :: thesis: for X being Subset of M st X = {} holds
X is sequentially_compact
let X be Subset of M; :: thesis: ( X = {} implies X is sequentially_compact )
assume A1: X = {} ; :: thesis: X is sequentially_compact
let S1 be sequence of M; :: according to TOPMETR4:def 1 :: thesis: ( rng S1 c= X implies 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 ) )
assume A2: rng S1 c= X ; :: thesis: 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 )
S1 . 0 in rng S1 by FUNCT_2:4;
hence 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 ) by A1, A2; :: thesis: verum