let M be finite-degree Matroid; :: thesis: for A being Subset of M st A is cycle holds

( not A is empty & A is finite )

let A be Subset of M; :: thesis: ( A is cycle implies ( not A is empty & A is finite ) )

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 & A is finite )

thus not A is empty by A1; :: thesis: A is finite

set e = the Element of A;

( not A is empty & A is finite )

let A be Subset of M; :: thesis: ( A is cycle implies ( not A is empty & A is finite ) )

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 & A is finite )

thus not A is empty by A1; :: thesis: A is finite

set e = the Element of A;

now :: thesis: ( A is non empty set implies A is finite )

hence
A is finite
; :: thesis: verumassume A3:
A is non empty set
; :: thesis: A is finite

then the Element of A in A ;

then reconsider e = the Element of A as Element of M ;

reconsider Ae = A \ {e} as independent Subset of M by A2, A3;

A = Ae \/ {e} by A3, ZFMISC_1:116;

hence A is finite ; :: thesis: verum

end;then the Element of A in A ;

then reconsider e = the Element of A as Element of M ;

reconsider Ae = A \ {e} as independent Subset of M by A2, A3;

A = Ae \/ {e} by A3, ZFMISC_1:116;

hence A is finite ; :: thesis: verum