let M be finite-degree Matroid; :: thesis: for A being Subset of M
for e, f being Element of M st Rnk (A \/ {e}) = Rnk (A \/ {f}) & Rnk (A \/ {f}) = Rnk A holds
Rnk (A \/ {e,f}) = Rnk A
let A be Subset of M; :: thesis: for e, f being Element of M st Rnk (A \/ {e}) = Rnk (A \/ {f}) & Rnk (A \/ {f}) = Rnk A holds
Rnk (A \/ {e,f}) = Rnk A
let e, f be Element of M; :: thesis: ( Rnk (A \/ {e}) = Rnk (A \/ {f}) & Rnk (A \/ {f}) = Rnk A implies Rnk (A \/ {e,f}) = Rnk A )
consider C being independent Subset of M such that
A0: ( C c= A & card C = Rnk A ) by ThR1;
( A c= A \/ {e,f} & A c= A \/ {e} & A c= A \/ {f} ) by XBOOLE_1:7;
then A6: ( C c= A \/ {e,f} & C c= A \/ {e} & C c= A \/ {f} ) by A0, XBOOLE_1:1;
then consider C' being independent Subset of M such that
A1: ( C c= C' & C' is_maximal_independent_in A \/ {e,f} ) by Th;
A2: ( card C' = Rnk (A \/ {e,f}) & C is_maximal_independent_in A & C' c= A \/ {e,f} ) by A0, A1, ThR2;
assume ( Rnk (A \/ {e}) = Rnk (A \/ {f}) & Rnk (A \/ {f}) = Rnk A ) ; :: thesis: Rnk (A \/ {e,f}) = Rnk A
then A3: ( C is_maximal_independent_in A \/ {e} & C is_maximal_independent_in A \/ {f} ) by A0, A6, ThR2;

now

assume C' <> C ; :: thesis: contradiction
then consider x being set such that
A4: ( ( x in C' & not x in C ) or ( x in C & not x in C' ) ) by TARSKI:2;
{x} c= C' by A1, A4, ZFMISC_1:37;
then C \/ {x} c= C' by A1, XBOOLE_1:8;
then reconsider Cx = C \/ {x} as independent Subset of M by M1, XBOOLE_1:1;

now

assume x in A ; :: thesis: contradiction
then {x} c= A by ZFMISC_1:37;
then ( Cx c= A & C c= Cx ) by A0, XBOOLE_1:8, XBOOLE_1:7;
then C = Cx by A2, MAXIMAL;
then {x} c= C by XBOOLE_1:7;
hence contradiction by A1, A4, ZFMISC_1:37; :: thesis: verum

end;

then x in {e,f} by A1, A2, A4, XBOOLE_0:def 3;
then ( x = e or x = f ) by TARSKI:def 2;
then ( ( {x} c= A \/ {e} & C c= A \/ {e} ) or ( {x} c= A \/ {f} & C c= A \/ {f} ) ) by A0, XBOOLE_1:10;
then ( C c= Cx & ( Cx c= A \/ {e} or Cx c= A \/ {f} ) ) by XBOOLE_1:8, XBOOLE_1:7;
then C = Cx by A3, MAXIMAL;
then {x} c= C by XBOOLE_1:7;
hence contradiction by A1, A4, ZFMISC_1:37; :: thesis: verum

end;

hence Rnk (A \/ {e,f}) = Rnk A by A0, A2; :: thesis: verum