:: deftheorem Def15 defines Lim YELLOW_6:def 15 :
for T being non empty TopSpace
for N being net of T
for b₃ being Subset of T holds
( b₃ = Lim N iff for p being Point of T holds
( p in b₃ iff for V being a_neighborhood of p holds N is_eventually_in V ) );