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