let T be non empty TopStruct ; :: thesis: for S being sequence of T st not S is convergent holds
Lim S = {}
let S be sequence of T; :: thesis: ( not S is convergent implies Lim S = {} )
assume A1: not S is convergent ; :: thesis: Lim S = {}
set x = the Element of Lim S;
assume A2: Lim S <> {} ; :: thesis: contradiction
then the Element of Lim S in Lim S ;
then reconsider x = the Element of Lim S as Point of T ;
S is_convergent_to x by A2, FRECHET:def 5;
hence contradiction by A1; :: thesis: verum