let V be RealLinearSpace; :: thesis: for W being Subspace of V st V is finite-dimensional holds
W is finite-dimensional
let W be Subspace of V; :: thesis: ( V is finite-dimensional implies W is finite-dimensional )
assume A1: V is finite-dimensional ; :: thesis: W is finite-dimensional
consider A being Basis of W;
consider I being Basis of V such that
A2: A c= I by Th17;
I is finite by A1, Th24;
then A is finite by A2;
hence W is finite-dimensional by Def1; :: thesis: verum