let K be Ring; :: thesis: for V being LeftMod of K
for W being Subspace of V
for A being Subset of W holds A is Subset of V
let V be LeftMod of K; :: thesis: for W being Subspace of V
for A being Subset of W holds A is Subset of V
let W be Subspace of V; :: thesis: for A being Subset of W holds A is Subset of V
let A be Subset of W; :: thesis: A is Subset of V
the carrier of W c= the carrier of V by VECTSP_4:def 2;
hence A is Subset of V by XBOOLE_1:1; :: thesis: verum