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 )

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

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 A7:
for A, B being finite Subset of M st A is independent & B is independent & card B = (card A) + 1 holds
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;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

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