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