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

hence contradiction by A12; :: thesis: verum

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

then
D is independent
by A1, Th3;
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;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

hence contradiction by A12; :: thesis: verum