for p, q being Point of T st p in Lim N & q in Lim N holds
p = q by Th35;
hence Lim N is trivial by SUBSET_1:45; :: thesis: verum