:: deftheorem Def3 defines Subspaces_of RUSUB_4:def 3 :
for V being finite-dimensional RealUnitarySpace
for n being Element of NAT
for b₃ being set holds
( b₃ = n Subspaces_of V iff for x being object holds
( x in b₃ iff ex W being strict Subspace of V st
( W = x & dim W = n ) ) );