:: deftheorem defines a_filter YELLOW19:def 3 :
for T being non empty 1-sorted
for N being non empty NetStr over T holds a_filter N = { A where A is Subset of T : N is_eventually_in A } ;