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:
hence ( A \ {e} is independent & A \ {e} c= A ) by ; :: 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 ;
hence A \ {e} = B by ; :: 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
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