set M = LinearlyIndependentSubsets V;

A1: the_family_of (LinearlyIndependentSubsets V) = { A where A is Subset of V : A is linearly-independent } by Def8;

the carrier of (LinearlyIndependentSubsets V) = the carrier of V by Def8;

hence not the carrier of (LinearlyIndependentSubsets V) is empty ; :: according to STRUCT_0:def 1 :: thesis: ( not LinearlyIndependentSubsets V is void & LinearlyIndependentSubsets V is subset-closed )

{} V is linearly-independent ;

then {} in the_family_of (LinearlyIndependentSubsets V) by A1;

hence not the topology of (LinearlyIndependentSubsets V) is empty ; :: according to PENCIL_1:def 4 :: thesis: LinearlyIndependentSubsets V is subset-closed

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

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

then A2: ex A being Subset of V st

( x = A & A is linearly-independent ) by A1;

assume A3: y c= x ; :: thesis: y in the_family_of (LinearlyIndependentSubsets V)

then reconsider B = y as Subset of V by A2, XBOOLE_1:1;

B is linearly-independent by A2, A3, VECTSP_7:1;

hence y in the_family_of (LinearlyIndependentSubsets V) by A1; :: thesis: verum

A1: the_family_of (LinearlyIndependentSubsets V) = { A where A is Subset of V : A is linearly-independent } by Def8;

the carrier of (LinearlyIndependentSubsets V) = the carrier of V by Def8;

hence not the carrier of (LinearlyIndependentSubsets V) is empty ; :: according to STRUCT_0:def 1 :: thesis: ( not LinearlyIndependentSubsets V is void & LinearlyIndependentSubsets V is subset-closed )

{} V is linearly-independent ;

then {} in the_family_of (LinearlyIndependentSubsets V) by A1;

hence not the topology of (LinearlyIndependentSubsets V) is empty ; :: according to PENCIL_1:def 4 :: thesis: LinearlyIndependentSubsets V is subset-closed

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

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

then A2: ex A being Subset of V st

( x = A & A is linearly-independent ) by A1;

assume A3: y c= x ; :: thesis: y in the_family_of (LinearlyIndependentSubsets V)

then reconsider B = y as Subset of V by A2, XBOOLE_1:1;

B is linearly-independent by A2, A3, VECTSP_7:1;

hence y in the_family_of (LinearlyIndependentSubsets V) by A1; :: thesis: verum