theorem :: CARDFIL2:40

for X being non empty set
for A being non empty Subset of X
for F being Filter of A
for B being basis of F holds
( (incl A) .: (# B) is filter_base of X & <.((incl A) .: (# B)).] is Filter of X & <.((incl A) .: (# B)).] = { M where M is Subset of X : (incl A) " M in F } ) by Th12;