let F be Ring; :: thesis: for V, W being VectSp of F

for X being Subset of V st V is Subspace of W holds

X is Subset of W

let V, W be VectSp of F; :: thesis: for X being Subset of V st V is Subspace of W holds

X is Subset of W

let X be Subset of V; :: thesis: ( V is Subspace of W implies X is Subset of W )

assume V is Subspace of W ; :: thesis: X is Subset of W

then A1: [#] V c= [#] W by VECTSP_4:def 2;

X c= [#] W by A1;

hence X is Subset of W ; :: thesis: verum

for X being Subset of V st V is Subspace of W holds

X is Subset of W

let V, W be VectSp of F; :: thesis: for X being Subset of V st V is Subspace of W holds

X is Subset of W

let X be Subset of V; :: thesis: ( V is Subspace of W implies X is Subset of W )

assume V is Subspace of W ; :: thesis: X is Subset of W

then A1: [#] V c= [#] W by VECTSP_4:def 2;

X c= [#] W by A1;

hence X is Subset of W ; :: thesis: verum