:: deftheorem defines elementary_filter CARDFIL2:def 17 :
for X being non empty set
for s being sequence of X holds elementary_filter s = filter_image (s,(Frechet_Filter NAT));