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

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;
let A be Subset of (); :: thesis: ( A is independent iff for D being Element of P ex d being Element of D st A /\ D c= {d} )
A2: the carrier of () = union P by Def7;
thus ( A is independent implies for D being Element of P ex d being Element of D st A /\ D c= {d} ) :: thesis: ( ( for D being Element of P ex d being Element of D st A /\ D c= {d} ) implies A is independent )
proof
assume A in the_family_of () ; :: according to MATROID0:def 2 :: thesis: for D being Element of P ex d being Element of D st A /\ D c= {d}
then A3: 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;
let D be Element of P; :: thesis: ex d being Element of D st A /\ D c= {d}
( P = {} implies ( A = {} & {} /\ D = {} ) ) by ;
then ( P = {} implies A /\ D c= {1} ) ;
then consider d being set such that
A4: A /\ D c= {d} by A3;
set d0 = the Element of D;
now :: thesis: ( d nin D implies A /\ D c= { the Element of D} )
assume d nin D ; :: thesis: A /\ D c= { the Element of D}
then d nin A /\ D by XBOOLE_0:def 4;
then A /\ D <> {d} by TARSKI:def 1;
then A /\ D = {} by ;
hence A /\ D c= { the Element of D} ; :: thesis: verum
end;
hence ex d being Element of D st A /\ D c= {d} by A4; :: thesis: verum
end;
assume A5: for D being Element of P ex d being Element of D st A /\ D c= {d} ; :: thesis: A is independent
A6: now :: thesis: for D being set st D in P holds
ex d being set st A /\ D c= {d}
let D be set ; :: thesis: ( D in P implies ex d being set st A /\ D c= {d} )
assume D in P ; :: thesis: ex d being set st A /\ D c= {d}
then ex d being Element of D st A /\ D c= {d} by A5;
hence ex d being set st A /\ D c= {d} ; :: thesis: verum
end;
the carrier of () = union P by Def7;
hence A in the_family_of () by A1, A6; :: according to MATROID0:def 2 :: thesis: verum