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