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
A0: not A is independent and
A1: 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 A0; :: thesis: A is finite
consider e being Element of A;

now

assume A is non empty set ; :: thesis: A is finite
then A2: e in A ;
then reconsider e = e as Element of M ;
reconsider Ae = A \ {e} as independent Subset of M by A1, A2;
A = Ae \/ {e} by A2, ZFMISC_1:140;
hence A is finite ; :: thesis: verum

end;

hence A is finite ; :: thesis: verum