bool the carrier of TS is finite ;
hence _bool TS is finite by Def1; :: thesis: verum