let F be Field; :: thesis: for V, W being VectSp of
for X being Subset of st V is Subspace of W holds
X is Subset of
let V, W be VectSp of ; :: thesis: for X being Subset of st V is Subspace of W holds
X is Subset of
let X be Subset of ; :: thesis: ( V is Subspace of W implies X is Subset of )
assume V is Subspace of W ; :: thesis: X is Subset of
then A1: [#] V c= [#] W by VECTSP_4:def 2;
X c= [#] W

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in X or x in [#] W )
assume x in X ; :: thesis: x in [#] W
then x in [#] V ;
hence x in [#] W by A1; :: thesis: verum

end;

hence X is Subset of ; :: thesis: verum