let S be Subset of ; :: 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