let M be finite-degree Matroid; :: thesis: for A being Subset of M st ( for B being Subset of M st B c= A holds
not B is cycle ) holds
A is independent

let A be Subset of M; :: thesis: ( ( for B being Subset of M st B c= A holds
not B is cycle ) implies A is independent )

assume A1: for B being Subset of M st B c= A holds
not B is cycle ; :: thesis: A is independent
consider C being independent Subset of M such that
A2: C c= A and
A3: card C = Rnk A by Th18;
per cases ( A c= C or A c/= C ) ;
suppose A c= C ; :: thesis: A is independent
end;
suppose A c/= C ; :: thesis: A is independent
then consider x being object such that
A4: x in A and
A5: x nin C ;
reconsider x = x as Element of M by A4;
A6: C c= C \/ {x} by ZFMISC_1:137;
defpred S1[ Nat] means ex B being independent Subset of M st
( card B = \$1 & B c= C & B \/ {x} is dependent );
A7: C \/ {x} c= A by ;
A8: ex n being Nat st S1[n]
proof
take n = Rnk A; :: thesis: S1[n]
take C ; :: thesis: ( card C = n & C c= C & C \/ {x} is dependent )
thus ( card C = n & C c= C ) by A3; :: thesis: C \/ {x} is dependent
assume A9: C \/ {x} is independent ; :: thesis: contradiction
C is_maximal_independent_in A by A2, A3, Th19;
then C = C \/ {x} by A7, A6, A9;
then {x} c= C by XBOOLE_1:7;
hence contradiction by A5, ZFMISC_1:31; :: thesis: verum
end;
consider n being Nat such that
A10: ( S1[n] & ( for k being Nat st S1[k] holds
n <= k ) ) from consider B being independent Subset of M such that
A11: card B = n and
A12: B c= C and
A13: B \/ {x} is dependent by A10;
A14: x nin B by ;
A15: B \/ {x} is cycle
proof
thus B \/ {x} is dependent by A13; :: according to MATROID0:def 16 :: thesis: for e being Element of M st e in B \/ {x} holds
(B \/ {x}) \ {e} is independent

let e be Element of M; :: thesis: ( e in B \/ {x} implies (B \/ {x}) \ {e} is independent )
set Be = B \ {e};
A16: B \ {e} c= B by XBOOLE_1:36;
assume A17: e in B \/ {x} ; :: thesis: (B \/ {x}) \ {e} is independent
per cases ( e in B or e = x ) by ;
suppose A18: e in B ; :: thesis: (B \/ {x}) \ {e} is independent
A19: e nin B \ {e} by ZFMISC_1:56;
B = (B \ {e}) \/ {e} by ;
then A20: n = (card (B \ {e})) + 1 by ;
assume A21: (B \/ {x}) \ {e} is dependent ; :: thesis: contradiction
(B \/ {x}) \ {e} = (B \ {e}) \/ {x} by ;
then n <= card (B \ {e}) by ;
hence contradiction by A20, NAT_1:13; :: thesis: verum
end;
end;
end;
B c= A by ;
then B \/ {x} c= A by ;
hence A is independent by ; :: thesis: verum
end;
end;