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