set M = LinearlyIndependentSubsets V;
the carrier of (LinearlyIndependentSubsets V) = the carrier of V by Def5;
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 )
A2: the_family_of (LinearlyIndependentSubsets V) = { A where A is Subset of V : A is linearly-independent } by Def5;
{} V is linearly-independent ;
then {} in the_family_of (LinearlyIndependentSubsets V) by A2;
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 consider A being Subset of V such that
A3: ( x = A & A is linearly-independent ) by A2;
assume A4: y c= x ; :: thesis: y in the_family_of (LinearlyIndependentSubsets V)
then reconsider B = y as Subset of V by A3, XBOOLE_1:1;
B is linearly-independent by A3, A4, VECTSP_7:2;
hence y in the_family_of (LinearlyIndependentSubsets V) by A2; :: thesis: verum