set S = { (Lin A) where A is Subset of V : ( A is linearly-independent & card A = n ) } ;
A1: for x being set holds
( x in { (Lin A) where A is Subset of V : ( A is linearly-independent & card A = n ) } iff ex W being strict Subspace of V st
( W = x & dim W = n ) )

proof

let x be set ; :: thesis: ( x in { (Lin A) where A is Subset of V : ( A is linearly-independent & card A = n ) } iff ex W being strict Subspace of V st
( W = x & dim W = n ) )

hereby :: thesis: ( ex W being strict Subspace of V st
( W = x & dim W = n ) implies x in { (Lin A) where A is Subset of V : ( A is linearly-independent & card A = n ) } )

assume x in { (Lin A) where A is Subset of V : ( A is linearly-independent & card A = n ) } ; :: thesis: ex W being strict Subspace of V st
( W = x & dim W = n )
then consider A being Subset of V such that
A2: x = Lin A and
A3: A is linearly-independent and
A4: card A = n ;
reconsider W = x as strict Subspace of V by A2;
dim W = n by A2, A3, A4, Th30;
hence ex W being strict Subspace of V st
( W = x & dim W = n ) ; :: thesis: verum

end;

given W being strict Subspace of V such that A5: W = x and
A6: dim W = n ; :: thesis: x in { (Lin A) where A is Subset of V : ( A is linearly-independent & card A = n ) }
consider A being finite Subset of W such that
A7: A is Basis of W by Def1;
reconsider A = A as Subset of W ;
A is linearly-independent by A7, RLVECT_3:def 3;
then reconsider B = A as linearly-independent Subset of V by Th15;
A8: x = Lin A by A5, A7, RLVECT_3:def 3
.= Lin B by Th21 ;
then card B = n by A5, A6, Th30;
hence x in { (Lin A) where A is Subset of V : ( A is linearly-independent & card A = n ) } by A8; :: thesis: verum

end;

take { (Lin A) where A is Subset of V : ( A is linearly-independent & card A = n ) } ; :: thesis: for x being set holds
( x in { (Lin A) where A is Subset of V : ( A is linearly-independent & card A = n ) } iff ex W being strict Subspace of V st
( W = x & dim W = n ) )
thus for x being set holds
( x in { (Lin A) where A is Subset of V : ( A is linearly-independent & card A = n ) } iff ex W being strict Subspace of V st
( W = x & dim W = n ) ) by A1; :: thesis: verum