theorem Th12: :: CARDFIL2:34

for X, Y being non empty set
for f being Function of X,Y
for F being Filter of X
for B being basis of F holds
( f .: (# B) is filter_base of Y & <.(f .: (# B)).] is Filter of Y & <.(f .: (# B)).] = { M where M is Subset of Y : f " M in F } )