:: deftheorem Def17 defines lim YELLOW_6:def 17 :
for T being non empty Hausdorff TopSpace
for N being convergent net of T
for b₃ being Element of T holds
( b₃ = lim N iff b₃ in Lim N );