set M = ProdMatroid P;
A1: the_family_of () = { A where A is Subset of () : for D being set st D in P holds
ex d being set st A /\ D c= {d}
}
by Def7;
set A = {} ();
now :: thesis: for D being set st D in P holds
ex d being set st ({} ()) /\ D c= {d}
let D be set ; :: thesis: ( D in P implies ex d being set st ({} ()) /\ D c= {d} )
assume D in P ; :: thesis: ex d being set st ({} ()) /\ D c= {d}
take d = {} ; :: thesis: ({} ()) /\ D c= {d}
thus ({} ()) /\ D c= {d} ; :: thesis: verum
end;
then {} () in the_family_of () by A1;
hence not the topology of () is empty ; :: according to PENCIL_1:def 4 :: thesis:
thus the_family_of () 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 () or b c/= a or b in the_family_of () )
assume that
A2: a in the_family_of () and
A3: b c= a ; :: thesis:
A4: ex B being Subset of () 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 ;
hence b /\ D c= {d} by A6; :: thesis: verum
end;
b is Subset of () by ;
hence b in the_family_of () by A1, A5; :: thesis: verum
end;