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