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
Z0: not A is independent and
Z2: 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 Z0; :: 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 )
assume Z1: e in A ; :: thesis: A \ {e} is_maximal_independent_in A
set Ae = A \ {e};
A1: A = (A \ {e}) \/ {e} by Z1, ZFMISC_1:140;
thus ( A \ {e} is independent & A \ {e} c= A ) by Z2, Z1, 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 ( B is independent & B c= A & A \ {e} c= B ) ; :: thesis: A \ {e} = B
hence A \ {e} = B by Z0, A1, BORSUK_5:2; :: thesis: verum

end;

consider a being Element of A;
assume that
Z4: not A is empty and
Z3: for e being Element of M st e in A holds
A \ {e} is_maximal_independent_in A ; :: thesis: A is cycle
a in A by Z4;
then reconsider a = a as Element of M ;
set Ae = A \ {a};
A2: A \ {a} is_maximal_independent_in A by Z4, Z3;
A3: A \ {a} c= A by XBOOLE_1:36;

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 A2, A3, MAXIMAL;
then a nin {a} by Z4, 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 Z3;
hence A \ {e} is independent by MAXIMAL; :: thesis: verum