for T being non empty Hausdorff TopSpace
for N being constant net of T holds lim N = the_value_of N