INT.Group , pi_1 S,x are_isomorphic by Th27;
hence not pi_1 S,x is finite by GROUP_6:85; :: thesis: verum