G .size() is finite by Th7;
hence G .size() is natural ; :: thesis: verum