let T be non empty TopStruct ; :: thesis: Cl_Seq ({} T) = {}
consider x being Element of Cl_Seq ({} T);
assume A1: Cl_Seq ({} T) <> {} ; :: thesis: contradiction
then x in Cl_Seq ({} T) ;
then reconsider x = x as Point of T ;
consider S being sequence of T such that
A2: ( rng S c= {} T & x in Lim S ) by A1, Def2;
rng S = {} by A2;
then dom S = {} by RELAT_1:65;
hence contradiction by NORMSP_1:17; :: thesis: verum