:: deftheorem Def5 defines meet VECTSP_8:def 5 :
for F being Field
for VS being strict VectSp of F
for G being non empty Subset of (Subspaces VS)
for b₄ being strict Subspace of VS holds
( b₄ = meet G iff the carrier of b₄ = meet ((carr VS) .: G) );