let M be finite-degree Matroid; :: thesis: for A being Subset of M
for e, f being Element of M st f nin Span A & f in Span (A \/ {e}) holds
e in Span (A \/ {f})
let A be Subset of M; :: thesis: for e, f being Element of M st f nin Span A & f in Span (A \/ {e}) holds
e in Span (A \/ {f})
let e, f be Element of M; :: thesis: ( f nin Span A & f in Span (A \/ {e}) implies e in Span (A \/ {f}) )
assume that
A1: f nin Span A and
A2: f in Span (A \/ {e}) ; :: thesis: e in Span (A \/ {f})
A3: Rnk A <= Rnk (A \/ {f}) by Th26;
A4: Rnk (A \/ {f}) <= (Rnk A) + 1 by Th26;
Rnk A <> Rnk (A \/ {f}) by A1, Th30;
then A5: Rnk (A \/ {f}) = (Rnk A) + 1 by A3, A4, NAT_1:9;
A6: (A \/ {f}) \/ {e} = A \/ ({f} \/ {e}) by XBOOLE_1:4;
A7: Rnk (A \/ {e}) <= (Rnk A) + 1 by Th26;
A8: (A \/ {e}) \/ {f} = A \/ ({e} \/ {f}) by XBOOLE_1:4;
A9: Rnk ((A \/ {e}) \/ {f}) = Rnk (A \/ {e}) by A2, Th30;
then Rnk (A \/ {f}) <= Rnk (A \/ {e}) by A6, A8, Th26;
then Rnk (A \/ {f}) = Rnk ((A \/ {f}) \/ {e}) by A9, A5, A6, A8, A7, XXREAL_0:1;
hence e in Span (A \/ {f}) by Th30; :: thesis: verum