theorem Th23: :: YELLOW_6:23

for S being non empty 1-sorted
for N being net of S
for X being set
for M being subnet of N st M = N " X holds
M is_eventually_in X