set S = singletons X;
singletons X is Basis of (bspace X) by Th40;
hence bspace X is finite-dimensional by MATRLIN:def 1; :: thesis: verum