:: deftheorem defines cycle MATROID0:def 16 :
for M being SubsetFamilyStr
for A being Subset of M holds
( A is cycle iff ( A is dependent & ( for e being Element of M st e in A holds
A \ {e} is independent ) ) );