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;
now :: thesis: ( A is non empty set implies A is finite )
assume 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;
hence A is finite ; :: thesis: verum