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 )

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;

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

( 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

set a = the Element of A;
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;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

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

let e be Element of M; :: thesis: ( e in A implies A \ {e} is independent )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;then A = A \ {a} by A9;

then a nin {a} by A7, XBOOLE_0:def 5;

hence contradiction by TARSKI:def 1; :: thesis: verum

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