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