let M be finite-degree Matroid; :: thesis: for A, B being Subset of M st A is cycle & B is cycle & A c= B holds

A = B

let A, B be Subset of M; :: thesis: ( A is cycle & B is cycle & A c= B implies A = B )

assume that

A1: A is dependent and

for e being Element of M st e in A holds

A \ {e} is independent and

B is dependent and

A2: for e being Element of M st e in B holds

B \ {e} is independent ; :: according to MATROID0:def 16 :: thesis: ( not A c= B or A = B )

assume that

A3: A c= B and

A4: A <> B ; :: thesis: contradiction

consider x being object such that

A5: ( ( x in A & not x in B ) or ( x in B & not x in A ) ) by A4, TARSKI:2;

reconsider x = x as Element of M by A5;

A6: A c= B \ {x} by A3, A5, ZFMISC_1:34;

B \ {x} is independent by A2, A3, A5;

hence contradiction by A1, A6, Th3; :: thesis: verum

A = B

let A, B be Subset of M; :: thesis: ( A is cycle & B is cycle & A c= B implies A = B )

assume that

A1: A is dependent and

for e being Element of M st e in A holds

A \ {e} is independent and

B is dependent and

A2: for e being Element of M st e in B holds

B \ {e} is independent ; :: according to MATROID0:def 16 :: thesis: ( not A c= B or A = B )

assume that

A3: A c= B and

A4: A <> B ; :: thesis: contradiction

consider x being object such that

A5: ( ( x in A & not x in B ) or ( x in B & not x in A ) ) by A4, TARSKI:2;

reconsider x = x as Element of M by A5;

A6: A c= B \ {x} by A3, A5, ZFMISC_1:34;

B \ {x} is independent by A2, A3, A5;

hence contradiction by A1, A6, Th3; :: thesis: verum