let V be finite-dimensional RealUnitarySpace; :: thesis: for W being Subspace of V

for n being Element of NAT holds n Subspaces_of W c= n Subspaces_of V

let W be Subspace of V; :: thesis: for n being Element of NAT holds n Subspaces_of W c= n Subspaces_of V

let n be Element of NAT ; :: 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 RUSUB_1:21;

W1 in n Subspaces_of V by A2, Def3;

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

for n being Element of NAT holds n Subspaces_of W c= n Subspaces_of V

let W be Subspace of V; :: thesis: for n being Element of NAT holds n Subspaces_of W c= n Subspaces_of V

let n be Element of NAT ; :: 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 RUSUB_1:21;

W1 in n Subspaces_of V by A2, Def3;

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