:: deftheorem Def2 defines SubVS-Family VECTSP_8:def 2 :
for F being Field
for VS being strict VectSp of F
for b₃ being set holds
( b₃ is SubVS-Family of VS iff for x being set st x in b₃ holds
x is Subspace of VS );