theorem Th8: :: MATROID0:8

for P being set
for A being Subset of (ProdMatroid P) holds
( A is independent iff for D being Element of P ex d being Element of D st A /\ D c= {d} )