theorem Th20: :: YELLOW_6:20

for S being non empty 1-sorted
for N being net of S holds N is_eventually_in the carrier of S