let M be non empty non void SubsetFamilyStr; :: thesis: ( 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 ) )
thus ( M is with_exchange_property implies 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 ) ) :: thesis: ( ( 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 ) ) implies M is with_exchange_property )

proof

assume A1: 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 ) ; :: according to MATROID0:def 4 :: thesis: 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 )
let A, B be finite Subset of M; :: thesis: ( A is independent & B is independent & card B = (card A) + 1 implies ex e being Element of M st
( e in B \ A & A \/ {e} is independent ) )
assume that
A2: A in the_family_of M and
A3: B in the_family_of M and
A4: card B = (card A) + 1 ; :: according to MATROID0:def 2 :: thesis: ex e being Element of M st
( e in B \ A & A \/ {e} is independent )
consider e being Element of M such that
A5: e in B \ A and
A6: A \/ {e} in the_family_of M by A1, A2, A3, A4;
take e ; :: thesis: ( e in B \ A & A \/ {e} is independent )
thus ( e in B \ A & A \/ {e} in the_family_of M ) by A5, A6; :: according to MATROID0:def 2 :: thesis: verum

end;

assume A7: 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 ) ; :: thesis: M is with_exchange_property
let A, B be finite Subset of M; :: according to MATROID0:def 4 :: thesis: ( A in the_family_of M & B in the_family_of M & card B = (card A) + 1 implies ex e being Element of M st
( e in B \ A & A \/ {e} in the_family_of M ) )
assume that
A8: A in the_family_of M and
A9: B in the_family_of M ; :: thesis: ( not card B = (card A) + 1 or ex e being Element of M st
( e in B \ A & A \/ {e} in the_family_of M ) )
A10: B is independent by A9;
assume A11: card B = (card A) + 1 ; :: thesis: ex e being Element of M st
( e in B \ A & A \/ {e} in the_family_of M )
A is independent by A8;
then consider e being Element of M such that
A12: e in B \ A and
A13: A \/ {e} is independent by A7, A10, A11;
take e ; :: thesis: ( e in B \ A & A \/ {e} in the_family_of M )
thus ( e in B \ A & A \/ {e} in the_family_of M ) by A12, A13; :: thesis: verum