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