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: for D being set st D in P holds
ex d being set st ({} (union P)) /\ D c= {d}

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

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: ProdMatroid P is subset-closed
thus the_family_of (ProdMatroid P) is subset-closed :: according to MATROID0:def 3 :: thesis: verum

proof

let a, b be set ; :: according to CLASSES1:def 1 :: thesis: ( not a in the_family_of (ProdMatroid P) or b c/= a or b in the_family_of (ProdMatroid P) )
assume that
A2: a in the_family_of (ProdMatroid P) and
A3: b c= a ; :: thesis: b in the_family_of (ProdMatroid P)
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: for D being set st D in P holds
ex d being set st b /\ D c= {d}

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

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: verum

end;