for p, q being Point of T st p in lim_filter F & q in lim_filter F holds
p = q by Th38;
hence lim_filter F is trivial by SUBSET_1:45; :: thesis: verum