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 )

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

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 A15:
for C being Subset of Mfor 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

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;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 card A = card B )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;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

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

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

hence
M is Matroid
; :: thesis: verum
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

hence contradiction by A18, A21, NAT_1:13; :: thesis: verum

end;( 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

then
card A = card B9
by A15, A20;
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;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

hence contradiction by A18, A21, NAT_1:13; :: thesis: verum