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;
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
proof
let x be object ; :: 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:31;
then C \/ {x} c= Ca by ;
then reconsider Cx = C \/ {x} as independent Subset of M by ;
x in B by ;
then x in A /\ B by ;
then {x} c= A /\ B by ZFMISC_1:31;
then A9: Cx c= A /\ B by ;
A10: C c= Cx by XBOOLE_1:7;
C is_maximal_independent_in A /\ B by A1, A2, Th19;
then C = Cx by ;
then {x} c= C by XBOOLE_1:7;
hence x in C by ZFMISC_1:31; :: thesis: verum
end;
A /\ B c= B by XBOOLE_1:17;
then C c= B by A1;
then C c= Ca /\ B by ;
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 ;
A15: C9 c= A \/ B by A13;
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 object ; :: 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:31;
then Ca \/ {x} c= C9 by ;
then reconsider Cax = Ca \/ {x} as independent Subset of M by ;
A18: now :: thesis: ( x in A implies x in Ca )end;
( x in B implies x in C9 /\ B ) by ;
hence x in Ca \/ (C9 /\ B) by ; :: thesis: verum
end;
let x be object ; :: 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 ; :: 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 ;
then A22: card (C9 /\ B) <= Rnk B by ;
A23: card C9 = Rnk (A \/ B) by ;
card Ca = Rnk A by ;
then Rnk (A \/ B) = ((Rnk A) + (card (C9 /\ B))) - (Rnk (A /\ B)) by ;
hence (Rnk (A \/ B)) + (Rnk (A /\ B)) <= (Rnk A) + (Rnk B) by ; :: thesis: verum