for S being non empty 1-sorted
for N being net of S
for A being Subset of S,N holds N is_eventually_in A