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
A0: not A is independent and
for e being Element of M st e in A holds
A \ {e} is independent and
not B is independent and
AA: 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 A1: ( A c= B & A <> B ) ; :: thesis: contradiction
then consider x being set such that
A2: ( ( x in A & not x in B ) or ( x in B & not x in A ) ) by TARSKI:2;
reconsider x = x as Element of M by A2;
( A c= B \ {x} & B \ {x} is independent ) by AA, A1, A2, ZFMISC_1:40;
hence contradiction by A0, M1; :: thesis: verum