reconsider F0 = F as basis of F by Th03;
( <.(f .: (# F0)).] is Filter of Y & <.(f .: (# F0)).] = { M where M is Subset of Y : f " M in F } ) by Th12;
hence { M where M is Subset of Y : f " M in F } is Filter of Y ; :: thesis: verum