for M being non empty non void SubsetFamilyStr holds
( M is with_exchange_property iff for A, B being finite Subset of M st A is independent & B is independent & card B = (card A) + 1 holds
ex e being Element of M st
( e in B \ A & A \/ {e} is independent ) )