set M = ProdMatroid P;
the carrier of (ProdMatroid P) = union P by Def7;
hence not the carrier of (ProdMatroid P) is empty ; :: according to STRUCT_0:def 1 :: thesis: verum