:: deftheorem defines Lim CARDFIL2:def 23 :
for T being non empty TopSpace
for B being filter_base of the carrier of T holds Lim B = lim_filter <.B.);