Subspaces VS is SubVS-Family of VS

proof

let x be set ; :: according to VECTSP_8:def 2 :: thesis: ( x in Subspaces VS implies x is Subspace of VS )
assume x in Subspaces VS ; :: thesis: x is Subspace of VS
then ex W being strict Subspace of VS st x = W by VECTSP_5:def 3;
hence x is Subspace of VS ; :: thesis: verum

end;

hence Subspaces VS is non empty SubVS-Family of VS ; :: thesis: verum