let M be finite-degree Matroid; :: thesis: for A, B being Subset of M
for e being Element of M holds
( Rnk A <= Rnk (A \/ B) & Rnk (A \/ {e}) <= (Rnk A) + 1 )
let A, B be Subset of M; :: thesis: for e being Element of M holds
( Rnk A <= Rnk (A \/ B) & Rnk (A \/ {e}) <= (Rnk A) + 1 )
let e be Element of M; :: thesis: ( Rnk A <= Rnk (A \/ B) & Rnk (A \/ {e}) <= (Rnk A) + 1 )
thus Rnk A <= Rnk (A \/ B) by R2, XBOOLE_1:7; :: thesis: Rnk (A \/ {e}) <= (Rnk A) + 1
A1: (Rnk (A \/ {e})) + (Rnk (A /\ {e})) <= (Rnk A) + (Rnk {e}) by R3;
A2: Rnk (A \/ {e}) <= (Rnk (A \/ {e})) + (Rnk (A /\ {e})) by NAT_1:11;
( Rnk {e} <= card {e} & card {e} = 1 ) by ThR3, CARD_1:50;
then (Rnk A) + (Rnk {e}) <= (Rnk A) + 1 by XREAL_1:8;
then (Rnk (A \/ {e})) + (Rnk (A /\ {e})) <= (Rnk A) + 1 by A1, XXREAL_0:2;
hence Rnk (A \/ {e}) <= (Rnk A) + 1 by A2, XXREAL_0:2; :: thesis: verum