set a = the Element of the topology of M;

reconsider a = the Element of the topology of M as Subset of M ;

take a ; :: thesis: a is independent

thus a in the_family_of M ; :: according to MATROID0:def 2 :: thesis: verum

reconsider a = the Element of the topology of M as Subset of M ;

take a ; :: thesis: a is independent

thus a in the_family_of M ; :: according to MATROID0:def 2 :: thesis: verum