theorem Th19: :: YELLOW19:19

for T being non empty 1-sorted
for A being set
for N being net of T st N is_eventually_in A holds
for S being subnet of N holds S is_eventually_in A