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

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

hence
T is sequential
by Th25; :: thesis: verum
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

then A = Cl A by A3;

hence A is closed by PRE_TOPC:22; :: thesis: verum

end;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

A c= Cl A
by PRE_TOPC:18;
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;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

then A = Cl A by A3;

hence A is closed by PRE_TOPC:22; :: thesis: verum