theorem :: CARDFIL2:20

for X being set
for B1, B2 being Subset-Family of X st B1,B2 are_equivalent_generators holds
<.B1.] = <.B2.] by Th05;