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
A1: A is independent and
A2: B is cycle and
A3: C is cycle and
A4: B c= A \/ {e} and
A5: C c= A \/ {e} ; :: thesis: B = C
not C c= A by A1, Th3, A3;
then consider c being object such that
A6: c in C and
A7: c nin A ;
c in {e} by ;
then A8: c = e by TARSKI:def 1;
not B c= A by A1, Th3, A2;
then consider b being object such that
A9: b in B and
A10: b nin A ;
assume A11: B <> C ; :: thesis: contradiction
b in {e} by ;
then b = e by TARSKI:def 1;
then e in B /\ C by ;
then consider D being Subset of M such that
A12: D is cycle and
A13: D c= (B \/ C) \ {e} by A2, A3, A11, Th43;
D c= A
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in D or x in A )
assume A14: x in D ; :: thesis: x in A
then x in B \/ C by ;
then A15: ( x in B or x in C ) by XBOOLE_0:def 3;
x nin {e} by ;
hence x in A by ; :: thesis: verum
end;
then D is independent by ;
hence contradiction by A12; :: thesis: verum