:: deftheorem defines with_exchange_property MATROID0:def 4 :
for M being SubsetFamilyStr holds
( M is with_exchange_property iff for A, B being finite Subset of M st A in the_family_of M & B in the_family_of M & card B = (card A) + 1 holds
ex e being Element of M st
( e in B \ A & A \/ {e} in the_family_of M ) );