bool the carrier of SA is finite ;
hence _bool SA is finite by Th14; :: thesis: verum