for T being non empty TopSpace
for N being net of T st N in NetUniv T holds
for p being Point of T st not p in Lim N holds
ex Y being subnet of N st
( Y in NetUniv T & ( for Z being subnet of Y holds not p in Lim Z ) )