let M be finite-degree Matroid; :: thesis: for A, B being Subset of M

for e being Element of M st A c= B & e is_dependent_on A holds

e is_dependent_on B

let A, B be Subset of M; :: thesis: for e being Element of M st A c= B & e is_dependent_on A holds

e is_dependent_on B

let e be Element of M; :: thesis: ( A c= B & e is_dependent_on A implies e is_dependent_on B )

assume that

A1: A c= B and

A2: Rnk (A \/ {e}) = Rnk A ; :: according to MATROID0:def 14 :: thesis: e is_dependent_on B

consider Ca being independent Subset of M such that

A3: Ca c= A and

A4: card Ca = Rnk A by Th18;

A5: Ca c= B by A1, A3;

B c= B \/ {e} by XBOOLE_1:7;

then Ca c= B \/ {e} by A5;

then consider E being independent Subset of M such that

A6: Ca c= E and

A7: E is_maximal_independent_in B \/ {e} by Th14;

Rnk B <= Rnk (B \/ {e}) by Th26;

hence Rnk (B \/ {e}) = Rnk B by A16, A8, NAT_1:9; :: according to MATROID0:def 14 :: thesis: verum

for e being Element of M st A c= B & e is_dependent_on A holds

e is_dependent_on B

let A, B be Subset of M; :: thesis: for e being Element of M st A c= B & e is_dependent_on A holds

e is_dependent_on B

let e be Element of M; :: thesis: ( A c= B & e is_dependent_on A implies e is_dependent_on B )

assume that

A1: A c= B and

A2: Rnk (A \/ {e}) = Rnk A ; :: according to MATROID0:def 14 :: thesis: e is_dependent_on B

consider Ca being independent Subset of M such that

A3: Ca c= A and

A4: card Ca = Rnk A by Th18;

A5: Ca c= B by A1, A3;

B c= B \/ {e} by XBOOLE_1:7;

then Ca c= B \/ {e} by A5;

then consider E being independent Subset of M such that

A6: Ca c= E and

A7: E is_maximal_independent_in B \/ {e} by Th14;

A8: now :: thesis: not Rnk (B \/ {e}) = (Rnk B) + 1

A16:
Rnk (B \/ {e}) <= (Rnk B) + 1
by Th26;
E c= B \/ {e}
by A7;

then A9: E = E /\ (B \/ {e}) by XBOOLE_1:28

.= (E /\ B) \/ (E /\ {e}) by XBOOLE_1:23 ;

E /\ {e} c= {e} by XBOOLE_1:17;

then A10: ( ( E /\ {e} = {} & card {} = 0 ) or ( E /\ {e} = {e} & card {e} = 1 ) ) by CARD_1:30, ZFMISC_1:33;

card (E /\ B) <= Rnk B by Th17, XBOOLE_1:17;

then A11: (card (E /\ B)) + 1 <= (Rnk B) + 1 by XREAL_1:6;

Ca c= A \/ {e} by A3, XBOOLE_1:10;

then A12: Ca is_maximal_independent_in A \/ {e} by A2, A4, Th19;

A13: Ca c= Ca \/ {e} by XBOOLE_1:10;

assume A14: Rnk (B \/ {e}) = (Rnk B) + 1 ; :: thesis: contradiction

then card E = (Rnk B) + 1 by A7, Th19;

then (Rnk B) + 1 <= (card (E /\ B)) + (card (E /\ {e})) by A9, CARD_2:43;

then (card (E /\ B)) + 1 <= (card (E /\ B)) + (card (E /\ {e})) by A11, XXREAL_0:2;

then e in E /\ {e} by A10, TARSKI:def 1, XREAL_1:6;

then e in E by XBOOLE_0:def 4;

then {e} c= E by ZFMISC_1:31;

then Ca \/ {e} c= E by A6, XBOOLE_1:8;

then A15: Ca \/ {e} is independent by Th3;

Ca \/ {e} c= A \/ {e} by A3, XBOOLE_1:9;

then Ca = Ca \/ {e} by A13, A15, A12;

then {e} c= Ca by XBOOLE_1:7;

then B = B \/ {e} by A5, XBOOLE_1:1, XBOOLE_1:12;

hence contradiction by A14; :: thesis: verum

end;then A9: E = E /\ (B \/ {e}) by XBOOLE_1:28

.= (E /\ B) \/ (E /\ {e}) by XBOOLE_1:23 ;

E /\ {e} c= {e} by XBOOLE_1:17;

then A10: ( ( E /\ {e} = {} & card {} = 0 ) or ( E /\ {e} = {e} & card {e} = 1 ) ) by CARD_1:30, ZFMISC_1:33;

card (E /\ B) <= Rnk B by Th17, XBOOLE_1:17;

then A11: (card (E /\ B)) + 1 <= (Rnk B) + 1 by XREAL_1:6;

Ca c= A \/ {e} by A3, XBOOLE_1:10;

then A12: Ca is_maximal_independent_in A \/ {e} by A2, A4, Th19;

A13: Ca c= Ca \/ {e} by XBOOLE_1:10;

assume A14: Rnk (B \/ {e}) = (Rnk B) + 1 ; :: thesis: contradiction

then card E = (Rnk B) + 1 by A7, Th19;

then (Rnk B) + 1 <= (card (E /\ B)) + (card (E /\ {e})) by A9, CARD_2:43;

then (card (E /\ B)) + 1 <= (card (E /\ B)) + (card (E /\ {e})) by A11, XXREAL_0:2;

then e in E /\ {e} by A10, TARSKI:def 1, XREAL_1:6;

then e in E by XBOOLE_0:def 4;

then {e} c= E by ZFMISC_1:31;

then Ca \/ {e} c= E by A6, XBOOLE_1:8;

then A15: Ca \/ {e} is independent by Th3;

Ca \/ {e} c= A \/ {e} by A3, XBOOLE_1:9;

then Ca = Ca \/ {e} by A13, A15, A12;

then {e} c= Ca by XBOOLE_1:7;

then B = B \/ {e} by A5, XBOOLE_1:1, XBOOLE_1:12;

hence contradiction by A14; :: thesis: verum

Rnk B <= Rnk (B \/ {e}) by Th26;

hence Rnk (B \/ {e}) = Rnk B by A16, A8, NAT_1:9; :: according to MATROID0:def 14 :: thesis: verum