for X being non empty set
for F being Filter of X
for B1, B2 being basis of F holds # B1, # B2 are_equivalent_generators