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