set S = { (Lin A) where A is Subset of V : ( A is linearly-independent & card A = n ) } ;
take { (Lin A) where A is Subset of V : ( A is linearly-independent & card A = n ) } ; :: thesis:
for x being object 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 object ; :: thesis:

hereby :: thesis:

assume x in { (Lin A) where A is Subset of V : ( A is linearly-independent & card A = n ) } ; :: thesis:
then A1: ex A being Subset of V st
( x = Lin A & A is linearly-independent & card A = n ) ;
then reconsider W = x as strict Subspace of V ;
dim W = n by A1, Th9;
hence ex W being strict Subspace of V st
( W = x & dim W = n ) ; :: thesis:

end;

given W being strict Subspace of V such that A2: W = x and
A3: dim W = n ; :: thesis:
consider A being finite Subset of W such that
A4: A is Basis of W by Def1;
reconsider A = A as Subset of W ;
A is linearly-independent by A4, RUSUB_3:def 2;
then reconsider B = A as linearly-independent Subset of V by RUSUB_3:22;
A5: x = Lin A by A2, A4, RUSUB_3:def 2
.= Lin B by RUSUB_3:28 ;
then card B = n by A2, A3, Th9;
hence x in { (Lin A) where A is Subset of V : ( A is linearly-independent & card A = n ) } by A5; :: thesis:

end;

hence for x being object 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 ) ) ; :: thesis: