:: deftheorem Def3 defines carr VECTSP_8:def 3 :
for F being Field
for VS being strict VectSp of F
for x being Element of Subspaces VS
for b₄ being Subset of VS holds
( b₄ = carr x iff ex X being Subspace of VS st
( x = X & b₄ = the carrier of X ) );