for T being non empty TopSpace
for x being Point of T holds x is_a_convergence_point_of NeighborhoodSystem x,T by Th3;