for p, q being Point of T st p in Lim N & q in Lim N holds
p = q by Th44;
hence Lim N is trivial by REALSET1:15; :: thesis: verum