let S be Subset of M; :: thesis: ( S is empty implies S is independent )
assume S is empty ; :: thesis: S is independent
hence S in the_family_of M by Th2; :: according to MATROID0:def 2 :: thesis: verum