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 A5, A6, A7, XBOOLE_0:def 3;
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 A4, A9, A10, XBOOLE_0:def 3;
then b = e by TARSKI:def 1;
then e in B /\ C by A9, A6, A8, XBOOLE_0:def 4;
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 A13, XBOOLE_0:def 5;
then A15: ( x in B or x in C ) by XBOOLE_0:def 3;
x nin {e} by A13, A14, XBOOLE_0:def 5;
hence x in A by A4, A5, A15, XBOOLE_0:def 3; :: thesis: verum
end;
then D is independent by A1, Th3;
hence contradiction by A12; :: thesis: verum