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 )
A1: card {e} = 1 by CARD_1:30;
thus Rnk A <= Rnk (A \/ B) by Th24, XBOOLE_1:7; :: thesis: Rnk (A \/ {e}) <= (Rnk A) + 1
A2: (Rnk (A \/ {e})) + (Rnk (A /\ {e})) <= (Rnk A) + (Rnk {e}) by Th25;
Rnk {e} <= card {e} by Th20;
then (Rnk A) + (Rnk {e}) <= (Rnk A) + 1 by A1, XREAL_1:6;
then A3: (Rnk (A \/ {e})) + (Rnk (A /\ {e})) <= (Rnk A) + 1 by A2, XXREAL_0:2;
Rnk (A \/ {e}) <= (Rnk (A \/ {e})) + (Rnk (A /\ {e})) by NAT_1:11;
hence Rnk (A \/ {e}) <= (Rnk A) + 1 by A3, XXREAL_0:2; :: thesis: verum