let M be finite-degree Matroid; :: thesis: for A, B being Subset of M holds (Rnk (A \/ B)) + (Rnk (A /\ B)) <= (Rnk A) + (Rnk B)
let A, B be Subset of M; :: thesis: (Rnk (A \/ B)) + (Rnk (A /\ B)) <= (Rnk A) + (Rnk B)
consider C being independent Subset of M such that
A0: ( C c= A /\ B & card C = Rnk (A /\ B) ) by ThR1;
( A /\ B c= A & A /\ B c= B ) by XBOOLE_1:17;
then A8: ( C c= A & C c= B ) by A0, XBOOLE_1:1;
then consider Ca being independent Subset of M such that
A2: ( C c= Ca & Ca is_maximal_independent_in A ) by Th;
A6: ( Ca c= A & A c= A \/ B ) by A2, MAXIMAL, XBOOLE_1:7;
then Ca c= A \/ B by XBOOLE_1:1;
then consider C' being independent Subset of M such that
A1: ( Ca c= C' & C' is_maximal_independent_in A \/ B ) by Th;
C' /\ B c= B by XBOOLE_1:17;
then consider Cb being independent Subset of M such that
A3: ( C' /\ B c= Cb & Cb is_maximal_independent_in B ) by Th;
A4: ( card Ca = Rnk A & card Cb = Rnk B & C' c= A \/ B & card C' = Rnk (A \/ B) ) by A1, A2, A3, ThR2;
A5: C' = Ca \/ (C' /\ B)

proof

thus C' c= Ca \/ (C' /\ B) :: according to XBOOLE_0:def 10 :: thesis: not Ca \/ (C' /\ B) c/= C'

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in C' or x in Ca \/ (C' /\ B) )
assume B1: x in C' ; :: thesis: x in Ca \/ (C' /\ B)
B3: ( x in B implies x in C' /\ B ) by B1, XBOOLE_0:def 4;
{x} c= C' by B1, ZFMISC_1:37;
then Ca \/ {x} c= C' by A1, XBOOLE_1:8;
then reconsider Cax = Ca \/ {x} as independent Subset of M by M1, XBOOLE_1:1;

now

assume x in A ; :: thesis: x in Ca
then {x} c= A by ZFMISC_1:37;
then ( Cax c= A & Ca c= Cax ) by A6, XBOOLE_1:7, XBOOLE_1:8;
then Ca = Cax by A2, MAXIMAL;
then {x} c= Ca by XBOOLE_1:7;
hence x in Ca by ZFMISC_1:37; :: thesis: verum

end;

hence x in Ca \/ (C' /\ B) by B1, B3, A4, XBOOLE_0:def 3; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in Ca \/ (C' /\ B) or x in C' )
assume x in Ca \/ (C' /\ B) ; :: thesis: x in C'
then ( x in Ca or x in C' /\ B ) by XBOOLE_0:def 3;
hence x in C' by A1, XBOOLE_0:def 4; :: thesis: verum

end;

A7: Ca /\ (C' /\ B) = (Ca /\ C') /\ B by XBOOLE_1:16
.= Ca /\ B by A1, XBOOLE_1:28 ;
Ca /\ B = C

proof

thus Ca /\ B c= C :: according to XBOOLE_0:def 10 :: thesis: not C c/= Ca /\ B

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in Ca /\ B or x in C )
assume x in Ca /\ B ; :: thesis: x in C
then B1: ( x in Ca & x in B ) by XBOOLE_0:def 4;
then {x} c= Ca by ZFMISC_1:37;
then C \/ {x} c= Ca by A2, XBOOLE_1:8;
then reconsider Cx = C \/ {x} as independent Subset of M by M1, XBOOLE_1:1;
x in A /\ B by B1, A6, XBOOLE_0:def 4;
then {x} c= A /\ B by ZFMISC_1:37;
then ( Cx c= A /\ B & C c= Cx & C is_maximal_independent_in A /\ B ) by A0, ThR2, XBOOLE_1:7, XBOOLE_1:8;
then C = Cx by MAXIMAL;
then {x} c= C by XBOOLE_1:7;
hence x in C by ZFMISC_1:37; :: thesis: verum

end;

thus not C c/= Ca /\ B by A8, A2, XBOOLE_1:19; :: thesis: verum

end;

then Rnk (A \/ B) = ((Rnk A) + (card (C' /\ B))) - (Rnk (A /\ B)) by A0, A4, A5, A7, CARD_2:64;
then ( (Rnk (A \/ B)) + (Rnk (A /\ B)) = (Rnk A) + (card (C' /\ B)) & card (C' /\ B) <= Rnk B ) by A3, A4, NAT_1:44;
hence (Rnk (A \/ B)) + (Rnk (A /\ B)) <= (Rnk A) + (Rnk B) by XREAL_1:8; :: thesis: verum