:: deftheorem defines lim_f CARDFIL2:def 28 :
for T being non empty TopSpace
for s being sequence of T holds lim_f s = lim_filter (elementary_filter s);