:: by Grzegorz Bancerek and Yasunari Shidama

::

:: Received July 30, 2008

:: Copyright (c) 2008-2012 Association of Mizar Users

begin

notation

let M be SubsetFamilyStr;

let A be Subset of M;

synonym independent A for open ;

antonym dependent A for open ;

end;
let A be Subset of M;

synonym independent A for open ;

antonym dependent A for open ;

:: deftheorem defines the_family_of MATROID0:def 1 :

for M being SubsetFamilyStr holds the_family_of M = the topology of M;

for M being SubsetFamilyStr holds the_family_of M = the topology of M;

definition

let M be SubsetFamilyStr;

let A be Subset of M;

compatibility

( A is independent iff A in the_family_of M ) by PRE_TOPC:def 2;

end;
let A be Subset of M;

compatibility

( A is independent iff A in the_family_of M ) by PRE_TOPC:def 2;

:: deftheorem Def2 defines independent MATROID0:def 2 :

for M being SubsetFamilyStr

for A being Subset of M holds

( A is independent iff A in the_family_of M );

for M being SubsetFamilyStr

for A being Subset of M holds

( A is independent iff A in the_family_of M );

definition

let M be SubsetFamilyStr;

end;
attr M is with_exchange_property means :: MATROID0:def 4

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 );

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 );

:: deftheorem Def3 defines subset-closed MATROID0:def 3 :

for M being SubsetFamilyStr holds

( M is subset-closed iff the_family_of M is subset-closed );

for M being SubsetFamilyStr holds

( M is subset-closed iff the_family_of M is subset-closed );

:: deftheorem defines with_exchange_property MATROID0:def 4 :

for M being SubsetFamilyStr holds

( M is with_exchange_property iff 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 ) );

for M being SubsetFamilyStr holds

( M is with_exchange_property iff 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 ) );

registration

existence

ex b_{1} being SubsetFamilyStr st

( b_{1} is strict & not b_{1} is empty & not b_{1} is void & b_{1} is finite & b_{1} is subset-closed & b_{1} is with_exchange_property )

end;
ex b

( b

proof end;

registration

let M be non void SubsetFamilyStr;

existence

ex b_{1} being Subset of M st b_{1} is independent

end;
existence

ex b

proof end;

registration
end;

theorem Th1: :: MATROID0:1

for M being non void subset-closed SubsetFamilyStr

for A being independent Subset of M

for B being set st B c= A holds

B is independent Subset of M

for A being independent Subset of M

for B being set st B c= A holds

B is independent Subset of M

proof end;

registration

let M be non void subset-closed SubsetFamilyStr;

existence

ex b_{1} being Subset of M st

( b_{1} is finite & b_{1} is independent )

end;
existence

ex b

( b

proof end;

definition
end;

registration

let M be non void subset-closed SubsetFamilyStr;

coherence

for b_{1} being Subset of M st b_{1} is empty holds

b_{1} is independent

end;
coherence

for b

b

proof end;

theorem Th3: :: MATROID0:3

for M being non void SubsetFamilyStr holds

( M is subset-closed iff for A, B being Subset of M st A is independent & B c= A holds

B is independent )

( M is subset-closed iff for A, B being Subset of M st A is independent & B c= A holds

B is independent )

proof end;

registration

let M be non void subset-closed SubsetFamilyStr;

let A be independent Subset of M;

let B be set ;

coherence

for b_{1} being Subset of M st b_{1} = A /\ B holds

b_{1} is independent

for b_{1} being Subset of M st b_{1} = B /\ A holds

b_{1} is independent
;

coherence

for b_{1} being Subset of M st b_{1} = A \ B holds

b_{1} is independent

end;
let A be independent Subset of M;

let B be set ;

coherence

for b

b

proof end;

coherence for b

b

coherence

for b

b

proof end;

theorem Th4: :: MATROID0:4

for M being non empty non void SubsetFamilyStr holds

( 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 ) )

( 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 ) )

proof end;

:: deftheorem Def6 defines finite-membered MATROID0:def 6 :

for M being SubsetFamilyStr holds

( M is finite-membered iff the_family_of M is finite-membered );

for M being SubsetFamilyStr holds

( M is finite-membered iff the_family_of M is finite-membered );

definition

let M be SubsetFamilyStr;

end;
attr M is finite-degree means :Def7: :: MATROID0:def 7

( M is finite-membered & ex n being Nat st

for A being finite Subset of M st A is independent holds

card A <= n );

( M is finite-membered & ex n being Nat st

for A being finite Subset of M st A is independent holds

card A <= n );

:: deftheorem Def7 defines finite-degree MATROID0:def 7 :

for M being SubsetFamilyStr holds

( M is finite-degree iff ( M is finite-membered & ex n being Nat st

for A being finite Subset of M st A is independent holds

card A <= n ) );

for M being SubsetFamilyStr holds

( M is finite-degree iff ( M is finite-membered & ex n being Nat st

for A being finite Subset of M st A is independent holds

card A <= n ) );

registration

coherence

for b_{1} being SubsetFamilyStr st b_{1} is finite-degree holds

b_{1} is finite-membered

for b_{1} being SubsetFamilyStr st b_{1} is finite holds

b_{1} is finite-degree

end;
for b

b

proof end;

coherence for b

b

proof end;

begin

registration

existence

ex b_{1} being set st

( b_{1} is mutually-disjoint & not b_{1} is empty & b_{1} is with_non-empty_elements )

end;
ex b

( b

proof end;

theorem :: MATROID0:6

for P being non empty mutually-disjoint with_non-empty_elements set

for f being Choice_Function of P holds f is one-to-one

for f being Choice_Function of P holds f is one-to-one

proof end;

registration

coherence

for b_{1} being discrete SubsetFamilyStr holds

( not b_{1} is void & b_{1} is subset-closed & b_{1} is with_exchange_property )

end;
for b

( not b

proof end;

definition

let P be set ;

ex b_{1} being strict SubsetFamilyStr st

( the carrier of b_{1} = union P & the_family_of b_{1} = { A where A is Subset of (union P) : for D being set st D in P holds

ex d being set st A /\ D c= {d} } )

for b_{1}, b_{2} being strict SubsetFamilyStr st the carrier of b_{1} = union P & the_family_of b_{1} = { A where A is Subset of (union P) : for D being set st D in P holds

ex d being set st A /\ D c= {d} } & the carrier of b_{2} = union P & the_family_of b_{2} = { A where A is Subset of (union P) : for D being set st D in P holds

ex d being set st A /\ D c= {d} } holds

b_{1} = b_{2}
;

end;
func ProdMatroid P -> strict SubsetFamilyStr means :Def8: :: MATROID0:def 8

( the carrier of it = union P & the_family_of it = { A where A is Subset of (union P) : for D being set st D in P holds

ex d being set st A /\ D c= {d} } );

existence ( the carrier of it = union P & the_family_of it = { A where A is Subset of (union P) : for D being set st D in P holds

ex d being set st A /\ D c= {d} } );

ex b

( the carrier of b

ex d being set st A /\ D c= {d} } )

proof end;

uniqueness for b

ex d being set st A /\ D c= {d} } & the carrier of b

ex d being set st A /\ D c= {d} } holds

b

:: deftheorem Def8 defines ProdMatroid MATROID0:def 8 :

for P being set

for b_{2} being strict SubsetFamilyStr holds

( b_{2} = ProdMatroid P iff ( the carrier of b_{2} = union P & the_family_of b_{2} = { A where A is Subset of (union P) : for D being set st D in P holds

ex d being set st A /\ D c= {d} } ) );

for P being set

for b

( b

ex d being set st A /\ D c= {d} } ) );

registration
end;

theorem Th8: :: MATROID0:8

for P being set

for A being Subset of (ProdMatroid P) holds

( A is independent iff for D being Element of P ex d being Element of D st A /\ D c= {d} )

for A being Subset of (ProdMatroid P) holds

( A is independent iff for D being Element of P ex d being Element of D st A /\ D c= {d} )

proof end;

registration
end;

theorem Th9: :: MATROID0:9

for P being mutually-disjoint set

for x being Subset of (ProdMatroid P) ex f being Function of x,P st

for a being set st a in x holds

a in f . a

for x being Subset of (ProdMatroid P) ex f being Function of x,P st

for a being set st a in x holds

a in f . a

proof end;

theorem Th10: :: MATROID0:10

for P being mutually-disjoint set

for x being Subset of (ProdMatroid P)

for f being Function of x,P st ( for a being set st a in x holds

a in f . a ) holds

( x is independent iff f is one-to-one )

for x being Subset of (ProdMatroid P)

for f being Function of x,P st ( for a being set st a in x holds

a in f . a ) holds

( x is independent iff f is one-to-one )

proof end;

registration
end;

registration
end;

registration

let X be set ;

coherence

for b_{1} being a_partition of X holds b_{1} is mutually-disjoint

end;
coherence

for b

proof end;

registration
end;

registration

let M be non void finite-membered SubsetFamilyStr;

coherence

for b_{1} being independent Subset of M holds b_{1} is finite

end;
coherence

for b

proof end;

definition

let F be Field;

let V be VectSp of F;

ex b_{1} being strict SubsetFamilyStr st

( the carrier of b_{1} = the carrier of V & the_family_of b_{1} = { A where A is Subset of V : A is linearly-independent } )

for b_{1}, b_{2} being strict SubsetFamilyStr st the carrier of b_{1} = the carrier of V & the_family_of b_{1} = { A where A is Subset of V : A is linearly-independent } & the carrier of b_{2} = the carrier of V & the_family_of b_{2} = { A where A is Subset of V : A is linearly-independent } holds

b_{1} = b_{2}
;

end;
let V be VectSp of F;

func LinearlyIndependentSubsets V -> strict SubsetFamilyStr means :Def9: :: MATROID0:def 9

( the carrier of it = the carrier of V & the_family_of it = { A where A is Subset of V : A is linearly-independent } );

existence ( the carrier of it = the carrier of V & the_family_of it = { A where A is Subset of V : A is linearly-independent } );

ex b

( the carrier of b

proof end;

uniqueness for b

b

:: deftheorem Def9 defines LinearlyIndependentSubsets MATROID0:def 9 :

for F being Field

for V being VectSp of F

for b_{3} being strict SubsetFamilyStr holds

( b_{3} = LinearlyIndependentSubsets V iff ( the carrier of b_{3} = the carrier of V & the_family_of b_{3} = { A where A is Subset of V : A is linearly-independent } ) );

for F being Field

for V being VectSp of F

for b

( b

registration

let F be Field;

let V be VectSp of F;

coherence

( not LinearlyIndependentSubsets V is empty & not LinearlyIndependentSubsets V is void & LinearlyIndependentSubsets V is subset-closed )

end;
let V be VectSp of F;

coherence

( not LinearlyIndependentSubsets V is empty & not LinearlyIndependentSubsets V is void & LinearlyIndependentSubsets V is subset-closed )

proof end;

theorem Th11: :: MATROID0:11

for F being Field

for V being VectSp of F

for A being Subset of (LinearlyIndependentSubsets V) holds

( A is independent iff A is linearly-independent Subset of V )

for V being VectSp of F

for A being Subset of (LinearlyIndependentSubsets V) holds

( A is independent iff A is linearly-independent Subset of V )

proof end;

theorem :: MATROID0:12

for F being Field

for V being VectSp of F

for A, B being finite Subset of V st B c= A holds

for v being Vector of V st v in Lin A & not v in Lin B holds

ex w being Vector of V st

( w in A \ B & w in Lin ((A \ {w}) \/ {v}) )

for V being VectSp of F

for A, B being finite Subset of V st B c= A holds

for v being Vector of V st v in Lin A & not v in Lin B holds

ex w being Vector of V st

( w in A \ B & w in Lin ((A \ {w}) \/ {v}) )

proof end;

theorem Th13: :: MATROID0:13

for F being Field

for V being VectSp of F

for A being Subset of V st A is linearly-independent holds

for a being Element of V st a nin the carrier of (Lin A) holds

A \/ {a} is linearly-independent

for V being VectSp of F

for A being Subset of V st A is linearly-independent holds

for a being Element of V st a nin the carrier of (Lin A) holds

A \/ {a} is linearly-independent

proof end;

registration

let F be Field;

let V be VectSp of F;

coherence

LinearlyIndependentSubsets V is with_exchange_property

end;
let V be VectSp of F;

coherence

LinearlyIndependentSubsets V is with_exchange_property

proof end;

registration

let F be Field;

let V be finite-dimensional VectSp of F;

coherence

LinearlyIndependentSubsets V is finite-membered

end;
let V be finite-dimensional VectSp of F;

coherence

LinearlyIndependentSubsets V is finite-membered

proof end;

begin

definition

let M be SubsetFamilyStr;

let A, C be Subset of M;

end;
let A, C be Subset of M;

pred A is_maximal_independent_in C means :Def10: :: MATROID0:def 10

( A is independent & A c= C & ( for B being Subset of M st B is independent & B c= C & A c= B holds

A = B ) );

( A is independent & A c= C & ( for B being Subset of M st B is independent & B c= C & A c= B holds

A = B ) );

:: deftheorem Def10 defines is_maximal_independent_in MATROID0:def 10 :

for M being SubsetFamilyStr

for A, C being Subset of M holds

( A is_maximal_independent_in C iff ( A is independent & A c= C & ( for B being Subset of M st B is independent & B c= C & A c= B holds

A = B ) ) );

for M being SubsetFamilyStr

for A, C being Subset of M holds

( A is_maximal_independent_in C iff ( A is independent & A c= C & ( for B being Subset of M st B is independent & B c= C & A c= B holds

A = B ) ) );

theorem Th14: :: MATROID0:14

for M being non void finite-degree SubsetFamilyStr

for C, A being Subset of M st A c= C & A is independent holds

ex B being independent Subset of M st

( A c= B & B is_maximal_independent_in C )

for C, A being Subset of M st A c= C & A is independent holds

ex B being independent Subset of M st

( A c= B & B is_maximal_independent_in C )

proof end;

theorem :: MATROID0:15

for M being non void subset-closed finite-degree SubsetFamilyStr

for C being Subset of M ex A being independent Subset of M st A is_maximal_independent_in C

for C being Subset of M ex A being independent Subset of M st A is_maximal_independent_in C

proof end;

theorem Th16: :: MATROID0:16

for M being non empty non void subset-closed finite-degree SubsetFamilyStr holds

( 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 )

( 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 )

proof end;

definition

let M be finite-degree Matroid;

let C be Subset of M;

union { (card A) where A is independent Subset of M : A c= C } is Nat

end;
let C be Subset of M;

func Rnk C -> Nat equals :: MATROID0:def 11

union { (card A) where A is independent Subset of M : A c= C } ;

coherence union { (card A) where A is independent Subset of M : A c= C } ;

union { (card A) where A is independent Subset of M : A c= C } is Nat

proof end;

:: deftheorem defines Rnk MATROID0:def 11 :

for M being finite-degree Matroid

for C being Subset of M holds Rnk C = union { (card A) where A is independent Subset of M : A c= C } ;

for M being finite-degree Matroid

for C being Subset of M holds Rnk C = union { (card A) where A is independent Subset of M : A c= C } ;

theorem Th17: :: MATROID0:17

for M being finite-degree Matroid

for C being Subset of M

for A being independent Subset of M st A c= C holds

card A <= Rnk C

for C being Subset of M

for A being independent Subset of M st A c= C holds

card A <= Rnk C

proof end;

theorem Th18: :: MATROID0:18

for M being finite-degree Matroid

for C being Subset of M ex A being independent Subset of M st

( A c= C & card A = Rnk C )

for C being Subset of M ex A being independent Subset of M st

( A c= C & card A = Rnk C )

proof end;

theorem Th19: :: MATROID0:19

for M being finite-degree Matroid

for C being Subset of M

for A being independent Subset of M holds

( A is_maximal_independent_in C iff ( A c= C & card A = Rnk C ) )

for C being Subset of M

for A being independent Subset of M holds

( A is_maximal_independent_in C iff ( A c= C & card A = Rnk C ) )

proof end;

theorem Th21: :: MATROID0:21

for M being finite-degree Matroid

for C being finite Subset of M holds

( C is independent iff card C = Rnk C )

for C being finite Subset of M holds

( C is independent iff card C = Rnk C )

proof end;

:: deftheorem defines Rnk MATROID0:def 12 :

for M being finite-degree Matroid holds Rnk M = Rnk ([#] M);

for M being finite-degree Matroid holds Rnk M = Rnk ([#] M);

definition

let M be non void finite-degree SubsetFamilyStr;

ex b_{1} being independent Subset of M st b_{1} is_maximal_independent_in [#] M

end;
mode Basis of M -> independent Subset of M means :Def13: :: MATROID0:def 13

it is_maximal_independent_in [#] M;

existence it is_maximal_independent_in [#] M;

ex b

proof end;

:: deftheorem Def13 defines Basis MATROID0:def 13 :

for M being non void finite-degree SubsetFamilyStr

for b_{2} being independent Subset of M holds

( b_{2} is Basis of M iff b_{2} is_maximal_independent_in [#] M );

for M being non void finite-degree SubsetFamilyStr

for b

( b

theorem :: MATROID0:23

for M being finite-degree Matroid

for A being independent Subset of M ex B being Basis of M st A c= B

for A being independent Subset of M ex B being Basis of M st A c= B

proof end;

theorem Th25: :: MATROID0:25

for M being finite-degree Matroid

for A, B being Subset of M holds (Rnk (A \/ B)) + (Rnk (A /\ B)) <= (Rnk A) + (Rnk B)

for A, B being Subset of M holds (Rnk (A \/ B)) + (Rnk (A /\ B)) <= (Rnk A) + (Rnk B)

proof end;

theorem Th26: :: MATROID0:26

for M being finite-degree Matroid

for A, B being Subset of M

for e being Element of M holds

( Rnk A <= Rnk (A \/ B) & Rnk (A \/ {e}) <= (Rnk A) + 1 )

for A, B being Subset of M

for e being Element of M holds

( Rnk A <= Rnk (A \/ B) & Rnk (A \/ {e}) <= (Rnk A) + 1 )

proof end;

theorem :: MATROID0:27

for M being finite-degree Matroid

for A being Subset of M

for e, f being Element of M st Rnk (A \/ {e}) = Rnk (A \/ {f}) & Rnk (A \/ {f}) = Rnk A holds

Rnk (A \/ {e,f}) = Rnk A

for A being Subset of M

for e, f being Element of M st Rnk (A \/ {e}) = Rnk (A \/ {f}) & Rnk (A \/ {f}) = Rnk A holds

Rnk (A \/ {e,f}) = Rnk A

proof end;

begin

:: deftheorem Def14 defines is_dependent_on MATROID0:def 14 :

for M being finite-degree Matroid

for e being Element of M

for A being Subset of M holds

( e is_dependent_on A iff Rnk (A \/ {e}) = Rnk A );

for M being finite-degree Matroid

for e being Element of M

for A being Subset of M holds

( e is_dependent_on A iff Rnk (A \/ {e}) = Rnk A );

theorem Th28: :: MATROID0:28

for M being finite-degree Matroid

for A being Subset of M

for e being Element of M st e in A holds

e is_dependent_on A

for A being Subset of M

for e being Element of M st e in A holds

e is_dependent_on A

proof end;

theorem Th29: :: MATROID0:29

for M being finite-degree Matroid

for A, B being Subset of M

for e being Element of M st A c= B & e is_dependent_on A holds

e is_dependent_on B

for A, B being Subset of M

for e being Element of M st A c= B & e is_dependent_on A holds

e is_dependent_on B

proof end;

definition

let M be finite-degree Matroid;

let A be Subset of M;

{ e where e is Element of M : e is_dependent_on A } is Subset of M

end;
let A be Subset of M;

func Span A -> Subset of M equals :: MATROID0:def 15

{ e where e is Element of M : e is_dependent_on A } ;

coherence { e where e is Element of M : e is_dependent_on A } ;

{ e where e is Element of M : e is_dependent_on A } is Subset of M

proof end;

:: deftheorem defines Span MATROID0:def 15 :

for M being finite-degree Matroid

for A being Subset of M holds Span A = { e where e is Element of M : e is_dependent_on A } ;

for M being finite-degree Matroid

for A being Subset of M holds Span A = { e where e is Element of M : e is_dependent_on A } ;

theorem Th30: :: MATROID0:30

for M being finite-degree Matroid

for A being Subset of M

for e being Element of M holds

( e in Span A iff Rnk (A \/ {e}) = Rnk A )

for A being Subset of M

for e being Element of M holds

( e in Span A iff Rnk (A \/ {e}) = Rnk A )

proof end;

theorem Th34: :: MATROID0:34

for M being finite-degree Matroid

for A being Subset of M

for e being Element of M st e is_dependent_on Span A holds

e is_dependent_on A

for A being Subset of M

for e being Element of M st e is_dependent_on Span A holds

e is_dependent_on A

proof end;

theorem :: MATROID0:36

for M being finite-degree Matroid

for A being Subset of M

for f, e being Element of M st f nin Span A & f in Span (A \/ {e}) holds

e in Span (A \/ {f})

for A being Subset of M

for f, e being Element of M st f nin Span A & f in Span (A \/ {e}) holds

e in Span (A \/ {f})

proof end;

definition

let M be SubsetFamilyStr;

let A be Subset of M;

end;
let A be Subset of M;

attr A is cycle means :Def16: :: MATROID0:def 16

( A is dependent & ( for e being Element of M st e in A holds

A \ {e} is independent ) );

( A is dependent & ( for e being Element of M st e in A holds

A \ {e} is independent ) );

:: deftheorem Def16 defines cycle MATROID0:def 16 :

for M being SubsetFamilyStr

for A being Subset of M holds

( A is cycle iff ( A is dependent & ( for e being Element of M st e in A holds

A \ {e} is independent ) ) );

for M being SubsetFamilyStr

for A being Subset of M holds

( A is cycle iff ( A is dependent & ( for e being Element of M st e in A holds

A \ {e} is independent ) ) );

theorem Th37: :: MATROID0:37

for M being finite-degree Matroid

for A being Subset of M st A is cycle holds

( not A is empty & A is finite )

for A being Subset of M st A is cycle holds

( not A is empty & A is finite )

proof end;

registration

let M be finite-degree Matroid;

coherence

for b_{1} being Subset of M st b_{1} is cycle holds

( not b_{1} is empty & b_{1} is finite )
by Th37;

end;
coherence

for b

( not b

theorem Th38: :: MATROID0:38

for M being finite-degree Matroid

for A being Subset of M holds

( A is cycle iff ( not A is empty & ( for e being Element of M st e in A holds

A \ {e} is_maximal_independent_in A ) ) )

for A being Subset of M holds

( A is cycle iff ( not A is empty & ( for e being Element of M st e in A holds

A \ {e} is_maximal_independent_in A ) ) )

proof end;

theorem :: MATROID0:40

for M being finite-degree Matroid

for A being Subset of M

for e being Element of M st A is cycle & e in A holds

e is_dependent_on A \ {e}

for A being Subset of M

for e being Element of M st A is cycle & e in A holds

e is_dependent_on A \ {e}

proof end;

theorem Th41: :: MATROID0:41

for M being finite-degree Matroid

for A, B being Subset of M st A is cycle & B is cycle & A c= B holds

A = B

for A, B being Subset of M st A is cycle & B is cycle & A c= B holds

A = B

proof end;

theorem Th42: :: MATROID0:42

for M being finite-degree Matroid

for A being Subset of M st ( for B being Subset of M st B c= A holds

not B is cycle ) holds

A is independent

for A being Subset of M st ( for B being Subset of M st B c= A holds

not B is cycle ) holds

A is independent

proof end;

theorem Th43: :: MATROID0:43

for M being finite-degree Matroid

for A, B being Subset of M

for e being Element of M st A is cycle & B is cycle & A <> B & e in A /\ B holds

ex C being Subset of M st

( C is cycle & C c= (A \/ B) \ {e} )

for A, B being Subset of M

for e being Element of M st A is cycle & B is cycle & A <> B & e in A /\ B holds

ex C being Subset of M st

( C is cycle & C c= (A \/ B) \ {e} )

proof end;

theorem :: MATROID0:44

for M being finite-degree Matroid

for A, B, C being Subset of M

for e being Element of M st A is independent & B is cycle & C is cycle & B c= A \/ {e} & C c= A \/ {e} holds

B = C

for A, B, C being Subset of M

for e being Element of M st A is independent & B is cycle & C is cycle & B c= A \/ {e} & C c= A \/ {e} holds

B = C

proof end;