let M be finite-degree Matroid; :: thesis: for A, B, C being Subset of M
for e being Element of M st A is independent & B is cycle & C is cycle & B c= A \/ {e} & C c= A \/ {e} holds
B = C
let A, B, C be Subset of M; :: thesis: for e being Element of M st A is independent & B is cycle & C is cycle & B c= A \/ {e} & C c= A \/ {e} holds
B = C
let e be Element of M; :: thesis: ( A is independent & B is cycle & C is cycle & B c= A \/ {e} & C c= A \/ {e} implies B = C )
assume that
A0: ( A is independent & B is cycle & C is cycle ) and
A1: ( B c= A \/ {e} & C c= A \/ {e} ) ; :: thesis: B = C

now

assume B c= A ; :: thesis: contradiction
then B is independent by A0, M1;
hence contradiction by A0, CYCLE; :: thesis: verum

end;

then consider b being set such that
A2: ( b in B & b nin A ) by TARSKI:def 3;
b in {e} by A1, A2, XBOOLE_0:def 3;
then A3: b = e by TARSKI:def 1;

now

assume C c= A ; :: thesis: contradiction
then C is independent by A0, M1;
hence contradiction by A0, CYCLE; :: thesis: verum

end;

then consider c being set such that
A4: ( c in C & c nin A ) by TARSKI:def 3;
c in {e} by A1, A4, XBOOLE_0:def 3;
then c = e by TARSKI:def 1;
then A5: e in B /\ C by A2, A3, A4, XBOOLE_0:def 4;
assume B <> C ; :: thesis: contradiction
then consider D being Subset of M such that
A6: ( D is cycle & D c= (B \/ C) \ {e} ) by A0, A5, C2;
D c= A

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in D or x in A )
assume x in D ; :: thesis: x in A
then A7: ( x in B \/ C & x nin {e} ) by A6, XBOOLE_0:def 5;
then ( x in B or x in C ) by XBOOLE_0:def 3;
hence x in A by A1, A7, XBOOLE_0:def 3; :: thesis: verum

end;

then D is independent by A0, M1;
hence contradiction by A6, CYCLE; :: thesis: verum