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 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 Def3;

reconsider W1 = W1 as strict Subspace of V by RLSUB_1:27;

W1 in n Subspaces_of V by A2, Def3;

hence x in n Subspaces_of V by A1; :: thesis: verum

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 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 Def3;

reconsider W1 = W1 as strict Subspace of V by RLSUB_1:27;

W1 in n Subspaces_of V by A2, Def3;

hence x in n Subspaces_of V by A1; :: thesis: verum