:: deftheorem defines the_family_of MATROID0:def 1 :
for M being SubsetFamilyStr holds the_family_of M = the topology of M;