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 )
assume that
A1: Rnk (A \/ {e}) = Rnk (A \/ {f}) and
A2: Rnk (A \/ {f}) = Rnk A ; :: thesis: Rnk (A \/ {e,f}) = Rnk A
consider C being independent Subset of M such that
A3: C c= A and
A4: card C = Rnk A by Th18;
A5: C is_maximal_independent_in A by A3, A4, Th19;
A c= A \/ {f} by XBOOLE_1:7;
then C c= A \/ {f} by A3;
then A6: C is_maximal_independent_in A \/ {f} by A4, A2, Th19;
A c= A \/ {e} by XBOOLE_1:7;
then C c= A \/ {e} by A3;
then A7: C is_maximal_independent_in A \/ {e} by A4, A1, A2, Th19;
A c= A \/ {e,f} by XBOOLE_1:7;
then C c= A \/ {e,f} by A3;
then consider C9 being independent Subset of M such that
A8: C c= C9 and
A9: C9 is_maximal_independent_in A \/ {e,f} by Th14;
A10: C9 c= A \/ {e,f} by A9;

now :: thesis: not C9 <> C

assume C9 <> C ; :: thesis: contradiction
then consider x being object such that
A11: ( ( x in C9 & not x in C ) or ( x in C & not x in C9 ) ) by TARSKI:2;
{x} c= C9 by A8, A11, ZFMISC_1:31;
then C \/ {x} c= C9 by A8, XBOOLE_1:8;
then reconsider Cx = C \/ {x} as independent Subset of M by Th3, XBOOLE_1:1;

now :: thesis: not x in A

assume x in A ; :: thesis: contradiction
then {x} c= A by ZFMISC_1:31;
then A12: Cx c= A by A3, XBOOLE_1:8;
C c= Cx by XBOOLE_1:7;
then C = Cx by A5, A12;
then {x} c= C by XBOOLE_1:7;
hence contradiction by A8, A11, ZFMISC_1:31; :: thesis: verum

end;

then x in {e,f} by A8, A10, A11, 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 A3, XBOOLE_1:10;
then A13: ( Cx c= A \/ {e} or Cx c= A \/ {f} ) by XBOOLE_1:8;
C c= Cx by XBOOLE_1:7;
then C = Cx by A7, A6, A13;
then {x} c= C by XBOOLE_1:7;
hence contradiction by A8, A11, ZFMISC_1:31; :: thesis: verum

end;

hence Rnk (A \/ {e,f}) = Rnk A by A4, A9, Th19; :: thesis: verum