Subspaces VS is SubVS-Family of VS

proof

hence
Subspaces VS is non empty SubVS-Family of VS
; :: thesis: verum
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;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