:: deftheorem defines filter_image CARDFIL2:def 13 :
for X, Y being non empty set
for f being Function of X,Y
for F being Filter of X holds filter_image (f,F) = { M where M is Subset of Y : f " M in F } ;