theorem Th05: :: CARDFIL2:19

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