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