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
Z0: ( A is cycle & B is cycle & A <> B & e in A /\ B ) and
Z1: for C being Subset of M st C is cycle holds
C c/= (A \/ B) \ {e} ; :: thesis: contradiction
A0: ( e in A & e in B ) by Z0, XBOOLE_0:def 4;
then reconsider Ae = A \ {e}, Be = B \ {e} as independent Subset of M by Z0, CYCLE;
A1: ( A = Ae \/ {e} & B = Be \/ {e} ) by A0, ZFMISC_1:140;
reconsider A' = A, B' = B as finite Subset of M by Z0;
A3: (Rnk (A \/ B)) + (Rnk (A /\ B)) <= (Rnk A) + (Rnk B) by R3;
B2: e in {e} by TARSKI:def 1;
then ( e nin Ae & e nin Be ) by XBOOLE_0:def 5;
then A4: ( card A' = (card Ae) + 1 & card B' = (card Be) + 1 ) by A1, CARD_2:54;
then ( (Rnk A) + 1 = (card Ae) + 1 & (Rnk B) + 1 = (card Be) + 1 ) by Z0, C4;
then A5: (card (A' \/ B')) + (card (A' /\ B')) = ((Rnk A) + 1) + ((Rnk B) + 1) by A4, HALLMAR1:1
.= (((Rnk A) + (Rnk B)) + 1) + 1 ;
((Rnk (A \/ B)) + (Rnk (A /\ B))) + 1 <= ((Rnk A) + (Rnk B)) + 1 by A3, XREAL_1:8;
then A7: (((Rnk (A \/ B)) + (Rnk (A /\ B))) + 1) + 1 <= (card (A' \/ B')) + (card (A' /\ B')) by A5, XREAL_1:8;
A9: ( A /\ B c= A & A /\ B c= B ) by XBOOLE_1:17;
A c/= A /\ B by Z0, C1, A9, XBOOLE_1:1;
then consider a being set such that
B0: ( a in A & a nin A /\ B ) by TARSKI:def 3;
reconsider a = a as Element of M by B0;
{a} misses A /\ B by B0, ZFMISC_1:56;
then ( A /\ B c= A \ {a} & A \ {a} is independent ) by Z0, A9, B0, CYCLE, XBOOLE_1:86;
then A /\ B is independent by M1;
then card (A' /\ B') = Rnk (A /\ B) by ThR4;
then Z2: (((Rnk (A \/ B)) + (Rnk (A /\ B))) + 1) + 1 = (((Rnk (A \/ B)) + 1) + 1) + (card (A' /\ B')) ;
for C being Subset of M st C c= (A \/ B) \ {e} holds
not C is cycle by Z1;
then reconsider C = (A \/ B) \ {e} as independent Subset of M by C3;
B1: ( e nin C & e in A \/ B ) by B2, A0, XBOOLE_0:def 3, XBOOLE_0:def 5;
then B3: C \/ {e} = A' \/ B' by ZFMISC_1:140;
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 )
( not A is independent & A c= A \/ B ) by Z0, CYCLE, XBOOLE_1:7;
then not A \/ B is independent by M1;
hence ( D is independent & D c= A \/ B & C c= D implies C = D ) by B3, BORSUK_5:2; :: thesis: verum

end;

then (Rnk (A \/ B)) + 1 = (card C) + 1 by ThR2
.= card (A' \/ B') by B1, B3, CARD_2:54 ;
hence contradiction by Z2, A7, NAT_1:13; :: thesis: verum