for X being non empty set
for L being non empty reflexive transitive RelStr
for f being Function of ([#] L),X
for F being Filter of X
for B being basis of F st [#] L is directed holds
( F is_filter-coarser_than filter_image (f,(Tails_Filter L)) iff B is_coarser_than f .: (# (Tails L)) )