begin
:: deftheorem defines the_family_of MATROID0:def 1 :
:: deftheorem Def2 defines independent MATROID0:def 2 :
:: deftheorem Def3 defines subset-closed MATROID0:def 3 :
:: deftheorem defines with_exchange_property MATROID0:def 4 :
theorem Th1:
theorem Th2:
theorem Th3:
theorem Th4:
:: deftheorem Def5 defines finite-membered MATROID0:def 5 :
:: deftheorem Def6 defines finite-membered MATROID0:def 6 :
:: deftheorem Def7 defines finite-degree MATROID0:def 7 :
begin
theorem Th5:
theorem
theorem
:: deftheorem Def8 defines ProdMatroid MATROID0:def 8 :
theorem Th8:
theorem Th9:
theorem Th10:
:: deftheorem Def9 defines LinearlyIndependentSubsets MATROID0:def 9 :
theorem Th11:
theorem
theorem Th13:
begin
:: deftheorem Def10 defines is_maximal_independent_in MATROID0:def 10 :
theorem Th14:
theorem
theorem Th16:
:: deftheorem defines Rnk MATROID0:def 11 :
theorem Th17:
theorem Th18:
theorem Th19:
theorem Th20:
theorem Th21:
:: deftheorem defines Rnk MATROID0:def 12 :
:: deftheorem Def13 defines Basis MATROID0:def 13 :
theorem
theorem
theorem Th24:
theorem Th25:
theorem Th26:
theorem
begin
:: deftheorem Def14 defines is_dependent_on MATROID0:def 14 :
theorem Th28:
theorem Th29:
:: deftheorem defines Span MATROID0:def 15 :
theorem Th30:
theorem Th31:
theorem
theorem Th33:
theorem Th34:
theorem
theorem
:: deftheorem Def16 defines cycle MATROID0:def 16 :
theorem Th37:
theorem Th38:
theorem Th39:
theorem
theorem Th41:
theorem Th42:
theorem Th43:
theorem