set S = singletons X;
singletons X is Basis of bspace X by Th41;
hence bspace X is finite-dimensional by MATRLIN:def 3; :: thesis: verum