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 ) )
consider e0 being Element of M;
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 00: 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 ( A in the_family_of M & B in the_family_of M & 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 )
then consider e being Element of M such that
01: ( e in B \ A & A \/ {e} in the_family_of M ) by 00;
take e ; :: thesis: ( e in B \ A & A \/ {e} is independent )
thus ( e in B \ A & A \/ {e} in the_family_of M ) by 01; :: according to MATROID0:def 2 :: thesis: verum

end;

assume 02: 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 ( A in the_family_of M & 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 ) )
then 03: ( A is independent & B is independent ) by Def8;
assume card B = (card A) + 1 ; :: thesis: ex e being Element of M st
( e in B \ A & A \/ {e} in the_family_of M )
then consider e being Element of M such that
04: ( e in B \ A & A \/ {e} is independent ) by 02, 03;
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 04, Def8; :: thesis: verum