let T be non empty TopStruct ; :: thesis: ( T is Frechet iff for A being Subset of T holds Cl A = Cl_Seq A )
thus ( T is Frechet implies for A being Subset of T holds Cl A = Cl_Seq A ) :: thesis: ( ( for A being Subset of T holds Cl A = Cl_Seq A ) implies T is Frechet )

proof

assume A1: T is Frechet ; :: thesis: for A being Subset of T holds Cl A = Cl_Seq A
let A be Subset of T; :: thesis: Cl A = Cl_Seq A
reconsider A9 = A as Subset of T ;
thus Cl A c= Cl_Seq A :: according to XBOOLE_0:def 10 :: thesis: Cl_Seq A c= Cl A

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Cl A or x in Cl_Seq A )
assume A2: x in Cl A ; :: thesis: x in Cl_Seq A
then reconsider x9 = x as Point of T ;
ex S being sequence of T st
( rng S c= A9 & x9 in Lim S ) by A1, A2;
hence x in Cl_Seq A by Def1; :: thesis: verum

end;

thus Cl_Seq A c= Cl A by Th14; :: thesis: verum

end;

assume A3: for A being Subset of T holds Cl A = Cl_Seq A ; :: thesis: T is Frechet
let A be Subset of T; :: according to FRECHET:def 6 :: thesis: for b₁ being Element of the carrier of T holds
( not b₁ in Cl A or ex b₂ being Element of K10(K11(omega, the carrier of T)) st
( rng b₂ c= A & b₁ in Lim b₂ ) )
let x be Point of T; :: thesis: ( not x in Cl A or ex b₁ being Element of K10(K11(omega, the carrier of T)) st
( rng b₁ c= A & x in Lim b₁ ) )
assume x in Cl A ; :: thesis: ex b₁ being Element of K10(K11(omega, the carrier of T)) st
( rng b₁ c= A & x in Lim b₁ )
then x in Cl_Seq A by A3;
hence ex b₁ being Element of K10(K11(omega, the carrier of T)) st
( rng b₁ c= A & x in Lim b₁ ) by Def1; :: thesis: verum