let M be non void SubsetFamilyStr; :: thesis: ( M is subset-closed iff for A, B being Subset of M st A is independent & B c= A holds

B is independent )

thus ( M is subset-closed implies for A, B being Subset of M st A is independent & B c= A holds

B is independent ) by Th1; :: thesis: ( ( for A, B being Subset of M st A is independent & B c= A holds

B is independent ) implies M is subset-closed )

assume A1: for A, B being Subset of M st A is independent & B c= A holds

B is independent ; :: thesis: M is subset-closed

let x, y be set ; :: according to CLASSES1:def 1,MATROID0:def 3 :: thesis: ( not x in the_family_of M or y c/= x or y in the_family_of M )

assume x in the_family_of M ; :: thesis: ( y c/= x or y in the_family_of M )

then A2: x is independent Subset of M by Def2;

assume y c= x ; :: thesis: y in the_family_of M

then y is independent Subset of M by A1, A2, XBOOLE_1:1;

hence y in the_family_of M by Def2; :: thesis: verum

B is independent )

thus ( M is subset-closed implies for A, B being Subset of M st A is independent & B c= A holds

B is independent ) by Th1; :: thesis: ( ( for A, B being Subset of M st A is independent & B c= A holds

B is independent ) implies M is subset-closed )

assume A1: for A, B being Subset of M st A is independent & B c= A holds

B is independent ; :: thesis: M is subset-closed

let x, y be set ; :: according to CLASSES1:def 1,MATROID0:def 3 :: thesis: ( not x in the_family_of M or y c/= x or y in the_family_of M )

assume x in the_family_of M ; :: thesis: ( y c/= x or y in the_family_of M )

then A2: x is independent Subset of M by Def2;

assume y c= x ; :: thesis: y in the_family_of M

then y is independent Subset of M by A1, A2, XBOOLE_1:1;

hence y in the_family_of M by Def2; :: thesis: verum