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