let GF be Field; :: thesis: for n being Nat
for V being finite-dimensional VectSp of GF
for W being Subspace of V holds n Subspaces_of W c= n Subspaces_of V
let n be Nat; :: thesis: for V being finite-dimensional VectSp of GF
for W being Subspace of V holds n Subspaces_of W c= n Subspaces_of V
let V be finite-dimensional VectSp of GF; :: thesis: for W being Subspace of V holds n Subspaces_of W c= n Subspaces_of V
let W be Subspace of V; :: thesis: n Subspaces_of W c= n Subspaces_of V
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in n Subspaces_of W or x in n Subspaces_of V )
assume x in n Subspaces_of W ; :: thesis: x in n Subspaces_of V
then consider W1 being strict Subspace of W such that
A1: W1 = x and
A2: dim W1 = n by Def2;
reconsider W1 = W1 as strict Subspace of V by VECTSP_4:26;
W1 in n Subspaces_of V by A2, Def2;
hence x in n Subspaces_of V by A1; :: thesis: verum