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 A0: ( A c= B & 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
A1: ( Ca c= A & card Ca = Rnk A ) by ThR1;
B4: Ca c= B by A0, A1, XBOOLE_1:1;
A5: B c= B \/ {e} by XBOOLE_1:7;
A4: ( Rnk B <= Rnk (B \/ {e}) & Rnk (B \/ {e}) <= (Rnk B) + 1 ) by R4;
Ca c= B \/ {e} by B4, A5, XBOOLE_1:1;
then consider E being independent Subset of M such that
A6: ( Ca c= E & E is_maximal_independent_in B \/ {e} ) by Th;

now

assume B1: Rnk (B \/ {e}) = (Rnk B) + 1 ; :: thesis: contradiction
then C1: card E = (Rnk B) + 1 by A6, ThR2;
card (E /\ B) <= Rnk B by ThR0, XBOOLE_1:17;
then C2: (card (E /\ B)) + 1 <= (Rnk B) + 1 by XREAL_1:8;
E c= B \/ {e} by A6, ThR2;
then E = E /\ (B \/ {e}) by XBOOLE_1:28
.= (E /\ B) \/ (E /\ {e}) by XBOOLE_1:23 ;
then (Rnk B) + 1 <= (card (E /\ B)) + (card (E /\ {e})) by C1, CARD_2:62;
then ( (card (E /\ B)) + 1 <= (card (E /\ B)) + (card (E /\ {e})) & E /\ {e} c= {e} ) by C2, XXREAL_0:2, XBOOLE_1:17;
then ( 1 <= card (E /\ {e}) & ( ( E /\ {e} = {} & card {} = 0 ) or ( E /\ {e} = {e} & card {e} = 1 ) ) ) by XREAL_1:8, ZFMISC_1:39, CARD_1:50;
then e in E /\ {e} by TARSKI:def 1;
then e in E by XBOOLE_0:def 4;
then {e} c= E by ZFMISC_1:37;
then A3: ( Ca \/ {e} c= E & Ca \/ {e} c= A \/ {e} & Ca c= A \/ {e} & Ca c= Ca \/ {e} ) by A1, A6, XBOOLE_1:8, XBOOLE_1:9, XBOOLE_1:10;
( Ca \/ {e} is independent & Ca is_maximal_independent_in A \/ {e} ) by A0, A1, A3, M1, ThR2;
then Ca = Ca \/ {e} by A3, MAXIMAL;
then {e} c= Ca by XBOOLE_1:7;
then B = B \/ {e} by B4, XBOOLE_1:1, XBOOLE_1:12;
hence contradiction by B1; :: thesis: verum

end;

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