:: deftheorem Def7 defines ProdMatroid MATROID0:def 8 :
for P being set
for b₂ being strict SubsetFamilyStr holds
( b₂ = ProdMatroid P iff ( the carrier of b₂ = union P & the_family_of b₂ = { A where A is Subset of (union P) : for D being set st D in P holds
ex d being set st A /\ D c= {d} } ) );