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;

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

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;

A16: Rnk (B \/ {e}) <= (Rnk B) + 1 by Th26;
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