theorem :: CARDFIL2:23

for X being non empty set
for F being Filter of X
for B being basis of F
for S being Subset-Family of X
for S1 being Subset of F st S = S1 & # B,S are_equivalent_generators holds
S1 is basis of F