let M be finite-degree Matroid; 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; ( ( 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
; 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
;
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 A2, A4, ZFMISC_1:137;
A8:
ex
n being
Nat st
S1[
n]
consider n being
Nat such that A10:
(
S1[
n] & ( for
k being
Nat st
S1[
k] holds
n <= k ) )
from NAT_1:sch 5(A8);
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 A5, A12;
A15:
B \/ {x} is
cycle
proof
thus
B \/ {x} is
dependent
by A13;
MATROID0:def 16 for e being Element of M st e in B \/ {x} holds
(B \/ {x}) \ {e} is independent
let e be
Element of
M;
( 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}
;
(B \/ {x}) \ {e} is independent
per cases
( e in B or e = x )
by A17, ZFMISC_1:136;
suppose A18:
e in B
;
(B \/ {x}) \ {e} is independent A19:
e nin B \ {e}
by ZFMISC_1:56;
B = (B \ {e}) \/ {e}
by A18, ZFMISC_1:116;
then A20:
n = (card (B \ {e})) + 1
by A11, A19, CARD_2:41;
assume A21:
(B \/ {x}) \ {e} is
dependent
;
contradiction
(B \/ {x}) \ {e} = (B \ {e}) \/ {x}
by A14, A18, XBOOLE_1:87, ZFMISC_1:11;
then
n <= card (B \ {e})
by A10, A12, A16, A21, XBOOLE_1:1;
hence
contradiction
by A20, NAT_1:13;
verum end;
end;
B c= A
by A2, A12;
then
B \/ {x} c= A
by A4, ZFMISC_1:137;
hence
A is
independent
by A1, A15;
verum end;