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
A1: C c= A /\ B and
A2: card C = Rnk (A /\ B) by Th18;
A /\ B c= A by XBOOLE_1:17;
then C c= A by A1, XBOOLE_1:1;
then consider Ca being independent Subset of M such that
A3: C c= Ca and
A4: Ca is_maximal_independent_in A by Th14;
A5: Ca c= A by A4, Def10;
A6: Ca /\ B c= C

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in Ca /\ B or x in C )
assume A7: x in Ca /\ B ; :: thesis: x in C
then A8: x in Ca by XBOOLE_0:def 4;
then {x} c= Ca by ZFMISC_1:37;
then C \/ {x} c= Ca by A3, XBOOLE_1:8;
then reconsider Cx = C \/ {x} as independent Subset of M by Th3, XBOOLE_1:1;
x in B by A7, XBOOLE_0:def 4;
then x in A /\ B by A5, A8, XBOOLE_0:def 4;
then {x} c= A /\ B by ZFMISC_1:37;
then A9: Cx c= A /\ B by A1, XBOOLE_1:8;
A10: C c= Cx by XBOOLE_1:7;
C is_maximal_independent_in A /\ B by A1, A2, Th19;
then C = Cx by A9, A10, Def10;
then {x} c= C by XBOOLE_1:7;
hence x in C by ZFMISC_1:37; :: thesis: verum

end;

A /\ B c= B by XBOOLE_1:17;
then C c= B by A1, XBOOLE_1:1;
then C c= Ca /\ B by A3, XBOOLE_1:19;
then A11: Ca /\ B = C by A6, XBOOLE_0:def 10;
A c= A \/ B by XBOOLE_1:7;
then Ca c= A \/ B by A5, XBOOLE_1:1;
then consider C9 being independent Subset of M such that
A12: Ca c= C9 and
A13: C9 is_maximal_independent_in A \/ B by Th14;
A14: Ca /\ (C9 /\ B) = (Ca /\ C9) /\ B by XBOOLE_1:16
.= Ca /\ B by A12, XBOOLE_1:28 ;
A15: C9 c= A \/ B by A13, Th19;
A16: C9 = Ca \/ (C9 /\ B)

proof

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

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in C9 or x in Ca \/ (C9 /\ B) )
assume A17: x in C9 ; :: thesis: x in Ca \/ (C9 /\ B)
then {x} c= C9 by ZFMISC_1:37;
then Ca \/ {x} c= C9 by A12, XBOOLE_1:8;
then reconsider Cax = Ca \/ {x} as independent Subset of M by Th3, XBOOLE_1:1;

A18: now

assume x in A ; :: thesis: x in Ca
then {x} c= A by ZFMISC_1:37;
then A19: Cax c= A by A5, XBOOLE_1:8;
Ca c= Cax by XBOOLE_1:7;
then Ca = Cax by A4, A19, Def10;
then {x} c= Ca by XBOOLE_1:7;
hence x in Ca by ZFMISC_1:37; :: thesis: verum

end;

( x in B implies x in C9 /\ B ) by A17, XBOOLE_0:def 4;
hence x in Ca \/ (C9 /\ B) by A15, A17, A18, XBOOLE_0:def 3; :: thesis: verum

end;

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

end;

C9 /\ B c= B by XBOOLE_1:17;
then consider Cb being independent Subset of M such that
A20: C9 /\ B c= Cb and
A21: Cb is_maximal_independent_in B by Th14;
card Cb = Rnk B by A21, Th19;
then A22: card (C9 /\ B) <= Rnk B by A20, NAT_1:44;
A23: card C9 = Rnk (A \/ B) by A13, Th19;
card Ca = Rnk A by A4, Th19;
then Rnk (A \/ B) = ((Rnk A) + (card (C9 /\ B))) - (Rnk (A /\ B)) by A2, A23, A16, A14, A11, CARD_2:64;
hence (Rnk (A \/ B)) + (Rnk (A /\ B)) <= (Rnk A) + (Rnk B) by A22, XREAL_1:8; :: thesis: verum