let M be finite-degree Matroid; :: thesis: for A, B being Subset of M
for e being Element of M st A is cycle & B is cycle & A <> B & e in A /\ B holds
ex C being Subset of M st
( C is cycle & C c= (A \/ B) \ {e} )
let A, B be Subset of M; :: thesis: for e being Element of M st A is cycle & B is cycle & A <> B & e in A /\ B holds
ex C being Subset of M st
( C is cycle & C c= (A \/ B) \ {e} )
let e be Element of M; :: thesis: ( A is cycle & B is cycle & A <> B & e in A /\ B implies ex C being Subset of M st
( C is cycle & C c= (A \/ B) \ {e} ) )
assume that
A1: A is cycle and
A2: B is cycle and
A3: A <> B and
A4: e in A /\ B and
A5: for C being Subset of M st C is cycle holds
C c/= (A \/ B) \ {e} ; :: thesis: contradiction
A6: e in A by A4, XBOOLE_0:def 4;
A /\ B c= B by XBOOLE_1:17;
then A c/= A /\ B by A1, A2, A3, Th41, XBOOLE_1:1;
then consider a being object such that
A7: a in A and
A8: a nin A /\ B ;
reconsider a = a as Element of M by A7;
{a} misses A /\ B by A8, ZFMISC_1:50;
then A9: A /\ B c= A \ {a} by XBOOLE_1:17, XBOOLE_1:86;
reconsider A9 = A, B9 = B as finite Subset of M by A1, A2;
(Rnk (A \/ B)) + (Rnk (A /\ B)) <= (Rnk A) + (Rnk B) by Th25;
then A10: ((Rnk (A \/ B)) + (Rnk (A /\ B))) + 1 <= ((Rnk A) + (Rnk B)) + 1 by XREAL_1:6;
A \ {a} is independent by A1, A7;
then A /\ B is independent by A9, Th3;
then A11: card (A9 /\ B9) = Rnk (A /\ B) by Th21;
for C being Subset of M st C c= (A \/ B) \ {e} holds
not C is cycle by A5;
then reconsider C = (A \/ B) \ {e} as independent Subset of M by Th42;
A12: e in {e} by TARSKI:def 1;
then A13: e nin C by XBOOLE_0:def 5;
A14: e in B by A4, XBOOLE_0:def 4;
then reconsider Ae = A \ {e}, Be = B \ {e} as independent Subset of M by A1, A2, A6;
A15: e nin Be by A12, XBOOLE_0:def 5;
B = Be \/ {e} by A14, ZFMISC_1:116;
then A16: card B9 = (card Be) + 1 by A15, CARD_2:41;
then A17: (Rnk B) + 1 = (card Be) + 1 by A2, Th39;
A18: e nin Ae by A12, XBOOLE_0:def 5;
A = Ae \/ {e} by A6, ZFMISC_1:116;
then A19: card A9 = (card Ae) + 1 by A18, CARD_2:41;
then (Rnk A) + 1 = (card Ae) + 1 by A1, Th39;
then (card (A9 \/ B9)) + (card (A9 /\ B9)) = ((Rnk A) + 1) + ((Rnk B) + 1) by A19, A16, A17, HALLMAR1:1
.= (((Rnk A) + (Rnk B)) + 1) + 1 ;
then A20: (((Rnk (A \/ B)) + (Rnk (A /\ B))) + 1) + 1 <= (card (A9 \/ B9)) + (card (A9 /\ B9)) by A10, XREAL_1:6;
e in A \/ B by A6, XBOOLE_0:def 3;
then A21: C \/ {e} = A9 \/ B9 by ZFMISC_1:116;
C is_maximal_independent_in A \/ B

proof

thus ( C is independent & C c= A \/ B ) by XBOOLE_1:36; :: according to MATROID0:def 10 :: thesis: for B being Subset of M st B is independent & B c= A \/ B & C c= B holds
C = B
let D be Subset of M; :: thesis: ( D is independent & D c= A \/ B & C c= D implies C = D )
A22: A c= A \/ B by XBOOLE_1:7;
A is dependent by A1;
then A \/ B is dependent by A22, Th3;
hence ( D is independent & D c= A \/ B & C c= D implies C = D ) by A21, ZFMISC_1:138; :: thesis: verum

end;

then (Rnk (A \/ B)) + 1 = (card C) + 1 by Th19
.= card (A9 \/ B9) by A13, A21, CARD_2:41 ;
hence contradiction by A20, A11, NAT_1:13; :: thesis: verum