let T be non empty TopStruct ; :: thesis: for A being Subset of T holds A c= Cl_Seq A
let A be Subset of T; :: thesis: A c= Cl_Seq A
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in A or x in Cl_Seq A )
assume A1: x in A ; :: thesis: x in Cl_Seq A
then reconsider x' = x as Point of T ;
ex S being sequence of T st
( rng S c= A & x' in Lim S )

proof

set S = NAT --> x';
take NAT --> x' ; :: thesis: ( rng (NAT --> x') c= A & x' in Lim (NAT --> x') )
{x'} c= A

proof

let x'' be set ; :: according to TARSKI:def 3 :: thesis: ( not x'' in {x'} or x'' in A )
assume x'' in {x'} ; :: thesis: x'' in A
hence x'' in A by A1, TARSKI:def 1; :: thesis: verum

end;

hence rng (NAT --> x') c= A by FUNCOP_1:14; :: thesis: x' in Lim (NAT --> x')
NAT --> x' is_convergent_to x' by FRECHET:23;
hence x' in Lim (NAT --> x') by FRECHET:def 4; :: thesis: verum

end;

hence x in Cl_Seq A by Def2; :: thesis: verum