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;

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

hence
Rnk (A \/ {e,f}) = Rnk A
by A4, A9, Th19; :: thesis: verumassume
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;

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;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

then
x in {e,f}
by A8, A10, A11, XBOOLE_0:def 3;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} 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

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