let M be finite-degree Matroid; :: thesis: for A, B being Subset of holds (Rnk (A \/ B)) + (Rnk (A /\ B)) <= (Rnk A) + (Rnk B)
let A, B be Subset of ; :: thesis: (Rnk (A \/ B)) + (Rnk (A /\ B)) <= (Rnk A) + (Rnk B)
consider C being independent Subset of 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 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 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 C' being independent Subset of such that
A12: Ca c= C' and
A13: C' is_maximal_independent_in A \/ B by Th14;
A14: Ca /\ (C' /\ B) = (Ca /\ C') /\ B by XBOOLE_1:16
.= Ca /\ B by A12, XBOOLE_1:28 ;
A15: C' c= A \/ B by A13, Th19;
A16: 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 A17: x in C' ; :: thesis: x in Ca \/ (C' /\ B)
then {x} c= C' by ZFMISC_1:37;
then Ca \/ {x} c= C' by A12, XBOOLE_1:8;
then reconsider Cax = Ca \/ {x} as independent Subset of 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 C' /\ B ) by A17, XBOOLE_0:def 4;
hence x in Ca \/ (C' /\ 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 \/ (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 A12, XBOOLE_0:def 4; :: thesis: verum

end;

C' /\ B c= B by XBOOLE_1:17;
then consider Cb being independent Subset of such that
A20: C' /\ B c= Cb and
A21: Cb is_maximal_independent_in B by Th14;
card Cb = Rnk B by A21, Th19;
then A22: card (C' /\ B) <= Rnk B by A20, NAT_1:44;
A23: card C' = Rnk (A \/ B) by A13, Th19;
card Ca = Rnk A by A4, Th19;
then Rnk (A \/ B) = ((Rnk A) + (card (C' /\ 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