let n be Element of NAT ; :: thesis: for V being finite-dimensional RealLinearSpace
for W being Subspace of V holds n Subspaces_of W c= n Subspaces_of V
let V be finite-dimensional RealLinearSpace; :: 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 set ; :: 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 Def4;
reconsider W1 = W1 as strict Subspace of V by RLSUB_1:27;
W1 in n Subspaces_of V by A2, Def4;
hence x in n Subspaces_of V by A1; :: thesis: verum