let T be non empty TopSpace; :: thesis: ( T is Frechet implies T is sequential )
assume A1: T is Frechet ; :: thesis: T is sequential
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
proof
let A be Subset of T; :: 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 A2: for S being sequence of T st S is convergent & rng S c= A holds
Lim S c= A ; :: thesis: A is closed
A3: Cl A c= A
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Cl A or x in A )
assume A4: x in Cl A ; :: thesis: x in A
then reconsider p = x as Point of T ;
consider S being sequence of T such that
A5: rng S c= A and
A6: p in Lim S by A1, A4;
S is_convergent_to p by A6, Def5;
then S is convergent ;
then Lim S c= A by A2, A5;
hence x in A by A6; :: thesis: verum
end;
A c= Cl A by PRE_TOPC:18;
then A = Cl A by A3;
hence A is closed by PRE_TOPC:22; :: thesis: verum
end;
hence T is sequential by Th25; :: thesis: verum