let T be non empty TopSpace; :: thesis: ( T is sequential & ( for A being Subset of T holds Cl_Seq (Cl_Seq A) = Cl_Seq A ) implies T is Frechet )
assume A1: T is sequential ; :: thesis: ( ex A being Subset of T st not Cl_Seq (Cl_Seq A) = Cl_Seq A or T is Frechet )
assume A2: for A being Subset of T holds Cl_Seq (Cl_Seq A) = Cl_Seq A ; :: thesis: T is Frechet
assume not T is Frechet ; :: thesis: contradiction
then consider A being Subset of T such that
A3: ex x being Point of T st
( x in Cl A & ( for S being sequence of T st rng S c= A holds
not x in Lim S ) ) ;
for Sq being sequence of T st Sq is convergent & rng Sq c= Cl_Seq A holds
Lim Sq c= Cl_Seq A
proof
let Sq be sequence of T; :: thesis: ( Sq is convergent & rng Sq c= Cl_Seq A implies Lim Sq c= Cl_Seq A )
assume that
Sq is convergent and
A4: rng Sq c= Cl_Seq A ; :: thesis: Lim Sq c= Cl_Seq A
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in Lim Sq or y in Cl_Seq A )
assume A5: y in Lim Sq ; :: thesis: y in Cl_Seq A
then reconsider y9 = y as Point of T ;
y9 in Cl_Seq (Cl_Seq A) by A4, A5, Def1;
hence y in Cl_Seq A by A2; :: thesis: verum
end;
then A6: Cl_Seq A is closed by A1;
consider x being Point of T such that
A7: x in Cl A and
A8: for S being sequence of T st rng S c= A holds
not x in Lim S by A3;
A c= Cl_Seq A by Th18;
then x in Cl_Seq A by A7, A6, PRE_TOPC:15;
hence contradiction by A8, Def1; :: thesis: verum