let T be non empty TopSpace; :: thesis: ( ( for A being Subset of T st ( for S being sequence of T st S is convergent & rng S c= A holds
Lim S c= A ) holds
A is closed ) implies T is sequential )
assume A1: for A being Subset of T st ( for S being sequence of T st S is convergent & rng S c= A holds
Lim S c= A ) holds
A is closed ; :: thesis: T is sequential
let A be Subset of T; :: according to FRECHET:def 7 :: thesis: ( A is closed iff for S being sequence of T st S is convergent & rng S c= A holds
Lim S c= A )
thus ( A is closed implies for S being sequence of T st S is convergent & rng S c= A holds
Lim S c= A ) by Th26; :: thesis: ( ( for S being sequence of T st S is convergent & rng S c= A holds
Lim S c= A ) implies A is closed )
assume for S being sequence of T st S is convergent & rng S c= A holds
Lim S c= A ; :: thesis: A is closed
hence A is closed by A1; :: thesis: verum