set M = ProdMatroid P;
A1: the_family_of (ProdMatroid P) = { 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} } by Def7;
set A = {} (union P);

now :: thesis:

let D be set ; :: thesis:
assume D in P ; :: thesis:
take d = {} ; :: thesis:
thus ({} (union P)) /\ D c= {d} ; :: thesis:

end;

then {} (union P) in the_family_of (ProdMatroid P) by A1;
hence not the topology of (ProdMatroid P) is empty ; :: according to PENCIL_1:def 4 :: thesis:
thus the_family_of (ProdMatroid P) is subset-closed :: according to MATROID0:def 3 :: thesis:

proof

let a, b be set ; :: according to CLASSES1:def 1 :: thesis:
assume that
A2: a in the_family_of (ProdMatroid P) and
A3: b c= a ; :: thesis:
A4: ex B being Subset of (union P) st
( a = B & ( for D being set st D in P holds
ex d being set st B /\ D c= {d} ) ) by A1, A2;

A5: now :: thesis:

let D be set ; :: thesis:
assume D in P ; :: thesis:
then consider d being set such that
A6: a /\ D c= {d} by A4;
take d = d; :: thesis:
b /\ D c= a /\ D by A3, XBOOLE_1:26;
hence b /\ D c= {d} by A6; :: thesis:

end;

b is Subset of (union P) by A3, A4, XBOOLE_1:1;
hence b in the_family_of (ProdMatroid P) by A1, A5; :: thesis:

end;