let M be non empty non void subset-closed finite-degree SubsetFamilyStr; :: thesis: ( M is Matroid iff for C being Subset of M
for A, B being independent Subset of M st A is_maximal_independent_in C & B is_maximal_independent_in C holds
card A = card B )

hereby :: thesis: ( ( for C being Subset of M
for A, B being independent Subset of M st A is_maximal_independent_in C & B is_maximal_independent_in C holds
card A = card B ) implies M is Matroid )

assume A0: M is Matroid ; :: thesis: for C being Subset of M
for A, B being independent Subset of M st A is_maximal_independent_in C & B is_maximal_independent_in C holds
card A = card B
let C be Subset of M; :: thesis: for A, B being independent Subset of M st A is_maximal_independent_in C & B is_maximal_independent_in C holds
card A = card B

B0: now

let A, B be independent Subset of M; :: thesis: ( A is_maximal_independent_in C & B is_maximal_independent_in C implies not card A < card B )
assume that
A1: ( A is_maximal_independent_in C & B is_maximal_independent_in C ) and
A2: card A < card B ; :: thesis: contradiction
(card A) + 1 <= card B by A2, NAT_1:13;
then (card A) + 1 c= card B by NAT_1:40;
then consider D being set such that
A3: ( D c= B & card D = (card A) + 1 ) by CARD_FIL:36;
reconsider D = D as finite Subset of M by A3, XBOOLE_1:1;
D is independent by A3, M1;
then consider e being Element of M such that
A4: ( e in D \ A & A \/ {e} is independent ) by A0, A3, M2;
D \ A c= D by XBOOLE_1:36;
then A5: ( D \ A c= B & B c= C & A c= C ) by A1, A3, MAXIMAL, XBOOLE_1:1;
then D \ A c= C by XBOOLE_1:1;
then {e} c= C by A4, ZFMISC_1:37;
then ( A c= A \/ {e} & A \/ {e} c= C ) by A5, XBOOLE_1:7, XBOOLE_1:8;
then A \/ {e} = A by A1, A4, MAXIMAL;
then {e} c= A by XBOOLE_1:7;
then e in A by ZFMISC_1:37;
hence contradiction by A4, XBOOLE_0:def 5; :: thesis: verum

end;

let A, B be independent Subset of M; :: thesis: ( A is_maximal_independent_in C & B is_maximal_independent_in C implies card A = card B )
assume A1: ( A is_maximal_independent_in C & B is_maximal_independent_in C ) ; :: thesis: card A = card B
( card A < card B or card B < card A or card A = card B ) by XXREAL_0:1;
hence card A = card B by A1, B0; :: thesis: verum

end;

assume A3: for C being Subset of M
for A, B being independent Subset of M st A is_maximal_independent_in C & B is_maximal_independent_in C holds
card A = card B ; :: thesis: M is Matroid
M is with_exchange_property

proof

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 ) )
reconsider C = A \/ B as Subset of M ;
assume A4: ( A in the_family_of M & B in the_family_of M & card B = (card A) + 1 ) ; :: thesis: ex e being Element of M st
( e in B \ A & A \/ {e} in the_family_of M )
assume A5: for e being Element of M st e in B \ A holds
not A \/ {e} in the_family_of M ; :: thesis: contradiction
reconsider A = A as independent Subset of M by A4, Def8;
A6: A is_maximal_independent_in C

proof

thus A in the_family_of M by A4; :: according to MATROID0:def 2,MATROID0:def 10 :: thesis: ( A c= C & ( for B being Subset of M st B is independent & B c= C & A c= B holds
A = B ) )
thus A c= C by XBOOLE_1:7; :: thesis: for B being Subset of M st B is independent & B c= C & A c= B holds
A = B
let D be Subset of M; :: thesis: ( D is independent & D c= C & A c= D implies A = D )
assume A7: ( D is independent & D c= C & A c= D ) ; :: thesis: A = D
assume ( not A c= D or not D c= A ) ; :: according to XBOOLE_0:def 10 :: thesis: contradiction
then consider e being set such that
A8: ( e in D & not e in A ) by A7, TARSKI:def 3;
reconsider e = e as Element of M by A8;
e in B by A7, A8, XBOOLE_0:def 3;
then e in B \ A by A8, XBOOLE_0:def 5;
then ( {e} c= D & not A \/ {e} in the_family_of M ) by A5, A8, ZFMISC_1:37;
then ( A \/ {e} c= D & not A \/ {e} is independent ) by A7, Def8, XBOOLE_1:8;
hence contradiction by A7, M1; :: thesis: verum

end;

( B c= C & B is independent ) by Def8, A4, XBOOLE_1:7;
then consider B' being independent Subset of M such that
B1: ( B c= B' & B' is_maximal_independent_in C ) by Th;
( card A = card B' & card B <= card B' ) by A3, A6, B1, NAT_1:44;
hence contradiction by A4, NAT_1:13; :: thesis: verum

end;

hence M is Matroid ; :: thesis: verum