for M being finite-degree Matroid
for A being Subset of M
for e being Element of M st e in A holds
e is_dependent_on A by ZFMISC_1:31, XBOOLE_1:12;