:: deftheorem Def16 defines convergent YELLOW_6:def 16 :
for T being non empty TopSpace
for N being net of T holds
( N is convergent iff Lim N <> {} );