let M be finite-degree Matroid; :: thesis: for A being Subset of M
for e being Element of M st e in A holds
e is_dependent_on A
let A be Subset of M; :: thesis: for e being Element of M st e in A holds
e is_dependent_on A
let e be Element of M; :: thesis: ( e in A implies e is_dependent_on A )
assume e in A ; :: thesis: e is_dependent_on A
then {e} c= A by ZFMISC_1:31;
hence Rnk (A \/ {e}) = Rnk A by XBOOLE_1:12; :: according to MATROID0:def 14 :: thesis: verum