let M be non empty non void subset-closed finite-degree SubsetFamilyStr; ( 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 ( ( 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
;
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 Blet C be
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 BA2:
now let A,
B be
independent Subset of
M;
( 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
;
contradictionA6:
A c= C
by A3, Def10;
(card A) + 1
<= card B
by A5, NAT_1:13;
then
(card A) + 1
c= card B
by NAT_1:40;
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, XBOOLE_1:1;
B c= C
by A4, Def10;
then
D \ A c= C
by A11, XBOOLE_1:1;
then
{e} c= C
by A9, ZFMISC_1:37;
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, Def10;
then
{e} c= A
by XBOOLE_1:7;
then
e in A
by ZFMISC_1:37;
hence
contradiction
by A9, XBOOLE_0:def 5;
verum end; let A,
B be
independent Subset of
M;
( 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
;
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;
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
; M is Matroid
M is with_exchange_property
proof
let A,
B be
finite Subset of
M;
MATROID0:def 4 ( 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
;
ex e being Element of M st
( e in B \ A & A \/ {e} in the_family_of M )
B is
independent
by A17, Def2;
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:44;
assume A22:
for
e being
Element of
M st
e in B \ A holds
not
A \/ {e} in the_family_of M
;
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;
MATROID0:def 2,
MATROID0:def 10 ( 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;
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;
( 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
;
A = D
assume
( not
A c= D or not
D c= A )
;
XBOOLE_0:def 10 contradiction
then consider e being
set such that A26:
e in D
and A27:
not
e in A
by A25, TARSKI:def 3;
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
by Def2;
{e} c= D
by A26, ZFMISC_1:37;
then
A \/ {e} c= D
by A25, XBOOLE_1:8;
hence
contradiction
by A23, A28, Th3;
verum
end;
then
card A = card B9
by A15, A20;
hence
contradiction
by A18, A21, NAT_1:13;
verum
end;
hence
M is Matroid
; verum