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 object ; :: 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 x9 = x as Point of T ;
ex S being sequence of T st
( rng S c= A & x9 in Lim S )

proof

set S = NAT --> x9;
take NAT --> x9 ; :: thesis: ( rng (NAT --> x9) c= A & x9 in Lim (NAT --> x9) )
{x9} c= A by A1, TARSKI:def 1;
hence rng (NAT --> x9) c= A by FUNCOP_1:8; :: thesis: x9 in Lim (NAT --> x9)
NAT --> x9 is_convergent_to x9 by FRECHET:22;
hence x9 in Lim (NAT --> x9) by FRECHET:def 5; :: thesis: verum

end;

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