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