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