:: deftheorem defines are_equivalent_generators CARDFIL2:def 9 :
for X being set
for B1, B2 being Subset-Family of X holds
( B1,B2 are_equivalent_generators iff ( ( for b1 being Element of B1 ex b2 being Element of B2 st b2 c= b1 ) & ( for b2 being Element of B2 ex b1 being Element of B1 st b1 c= b2 ) ) );