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 A1: 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

A2: now :: thesis: for A, B being independent Subset of M st A is_maximal_independent_in C & B is_maximal_independent_in C holds
not card A < card B

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
A3: A is_maximal_independent_in C and
A4: B is_maximal_independent_in C and
A5: card A < card B ; :: thesis: contradiction
A6: A c= C by A3;
(card A) + 1 <= card B by A5, NAT_1:13;
then Segm ((card A) + 1) c= Segm (card B) by NAT_1:39;
then consider D being set such that
A7: D c= B and
A8: card D = (card A) + 1 by CARD_FIL:36;
reconsider D = D as finite Subset of M by A7, XBOOLE_1:1;
D is independent by A7, Th3;
then consider e being Element of M such that
A9: e in D \ A and
A10: A \/ {e} is independent by A1, A8, Th4;
D \ A c= D by XBOOLE_1:36;
then A11: D \ A c= B by A7;
B c= C by A4;
then D \ A c= C by A11;
then {e} c= C by A9, ZFMISC_1:31;
then A12: A \/ {e} c= C by A6, XBOOLE_1:8;
A c= A \/ {e} by XBOOLE_1:7;
then A \/ {e} = A by A3, A10, A12;
then {e} c= A by XBOOLE_1:7;
then e in A by ZFMISC_1:31;
hence contradiction by A9, 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 that
A13: A is_maximal_independent_in C and
A14: 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 A2, A13, A14; :: thesis: verum

end;

assume A15: 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 that
A16: A in the_family_of M and
A17: B in the_family_of M and
A18: card B = (card A) + 1 ; :: thesis: ex e being Element of M st
( e in B \ A & A \/ {e} in the_family_of M )
B is independent by A17;
then consider B9 being independent Subset of M such that
A19: B c= B9 and
A20: B9 is_maximal_independent_in C by Th14, XBOOLE_1:7;
A21: card B <= card B9 by A19, NAT_1:43;
assume A22: 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 A16, Def2;
A is_maximal_independent_in C

proof

thus A in the_family_of M by A16; :: 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 that
A23: D is independent and
A24: D c= C and
A25: 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 object such that
A26: e in D and
A27: not e in A by A25;
reconsider e = e as Element of M by A26;
e in B by A24, A26, A27, XBOOLE_0:def 3;
then e in B \ A by A27, XBOOLE_0:def 5;
then not A \/ {e} in the_family_of M by A22;
then A28: not A \/ {e} is independent ;
{e} c= D by A26, ZFMISC_1:31;
then A \/ {e} c= D by A25, XBOOLE_1:8;
hence contradiction by A23, A28, Th3; :: thesis: verum

end;

then card A = card B9 by A15, A20;
hence contradiction by A18, A21, NAT_1:13; :: thesis: verum

end;

hence M is Matroid ; :: thesis: verum