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);

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

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}

then
{} (union P) in the_family_of (ProdMatroid P)
by A1;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;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

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;

hence b in the_family_of (ProdMatroid P) by A1, A5; :: thesis: verum

end;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}

b is Subset of (union P)
by A3, A4, XBOOLE_1:1;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;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

hence b in the_family_of (ProdMatroid P) by A1, A5; :: thesis: verum