theorem Th10: :: YELLOW19:10

for T being non empty 1-sorted
for N being non empty NetStr over T
for A being set holds
( A in a_filter N iff ( N is_eventually_in A & A is Subset of T ) )