let M be finite-degree Matroid; :: thesis: 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 ) ) )
let A be Subset of M; :: thesis: ( 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 ) ) )
thus ( A is cycle implies ( not A is empty & ( for e being Element of M st e in A holds
A \ {e} is_maximal_independent_in A ) ) ) :: thesis: ( not A is empty & ( for e being Element of M st e in A holds
A \ {e} is_maximal_independent_in A ) implies A is cycle )

proof

assume that
A1: A is dependent and
A2: for e being Element of M st e in A holds
A \ {e} is independent ; :: according to MATROID0:def 16 :: thesis: ( not A is empty & ( for e being Element of M st e in A holds
A \ {e} is_maximal_independent_in A ) )
thus not A is empty by A1; :: thesis: for e being Element of M st e in A holds
A \ {e} is_maximal_independent_in A
let e be Element of M; :: thesis: ( e in A implies A \ {e} is_maximal_independent_in A )
set Ae = A \ {e};
assume A3: e in A ; :: thesis: A \ {e} is_maximal_independent_in A
hence ( A \ {e} is independent & A \ {e} c= A ) by A2, XBOOLE_1:36; :: according to MATROID0:def 10 :: thesis: for B being Subset of M st B is independent & B c= A & A \ {e} c= B holds
A \ {e} = B
let B be Subset of M; :: thesis: ( B is independent & B c= A & A \ {e} c= B implies A \ {e} = B )
assume that
A4: B is independent and
A5: B c= A and
A6: A \ {e} c= B ; :: thesis: A \ {e} = B
A = (A \ {e}) \/ {e} by A3, ZFMISC_1:116;
hence A \ {e} = B by A1, A4, A5, A6, ZFMISC_1:138; :: thesis: verum

end;

set a = the Element of A;
assume that
A7: not A is empty and
A8: for e being Element of M st e in A holds
A \ {e} is_maximal_independent_in A ; :: thesis: A is cycle
the Element of A in A by A7;
then reconsider a = the Element of A as Element of M ;
set Ae = A \ {a};
A9: A \ {a} is_maximal_independent_in A by A7, A8;

hereby :: according to MATROID0:def 16 :: thesis: for e being Element of M st e in A holds
A \ {e} is independent

assume A is independent ; :: thesis: contradiction
then A = A \ {a} by A9;
then a nin {a} by A7, XBOOLE_0:def 5;
hence contradiction by TARSKI:def 1; :: thesis: verum

end;

let e be Element of M; :: thesis: ( e in A implies A \ {e} is independent )
assume e in A ; :: thesis: A \ {e} is independent
then A \ {e} is_maximal_independent_in A by A8;
hence A \ {e} is independent ; :: thesis: verum