consider r being positive real number , o being Point of (TOP-REAL 2), y being Point of (Tcircle o,r);
let S be being_simple_closed_curve SubSpace of TOP-REAL 2; :: thesis: for x being Point of S holds INT.Group , pi_1 S,x are_isomorphic
let x be Point of S; :: thesis: INT.Group , pi_1 S,x are_isomorphic
( INT.Group , pi_1 (Tcircle o,r),y are_isomorphic & pi_1 (Tcircle o,r),y, pi_1 S,x are_isomorphic ) by Lm16, TOPALG_3:35, TOPREALB:11;
hence INT.Group , pi_1 S,x are_isomorphic by GROUP_6:78; :: thesis: verum