let M be finite-degree Matroid; 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; (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;
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;
A6:
Ca /\ B c= C
A /\ B c= B
by XBOOLE_1:17;
then
C c= B
by A1;
then
C c= Ca /\ B
by A3, XBOOLE_1:19;
then A11:
Ca /\ B = C
by A6;
A c= A \/ B
by XBOOLE_1:7;
then
Ca c= A \/ B
by A5;
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;
A16:
C9 = Ca \/ (C9 /\ B)
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:43;
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:45;
hence
(Rnk (A \/ B)) + (Rnk (A /\ B)) <= (Rnk A) + (Rnk B)
by A22, XREAL_1:6; verum