set r = the positive Real;
set o = the Point of (TOP-REAL 2);
set y = the Point of (Tcircle ( the Point of (TOP-REAL 2), the positive Real));
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 ( the Point of (TOP-REAL 2), the positive Real)), the Point of (Tcircle ( the Point of (TOP-REAL 2), the positive Real))) are_isomorphic & pi_1 ((Tcircle ( the Point of (TOP-REAL 2), the positive Real)), the Point of (Tcircle ( the Point of (TOP-REAL 2), the positive Real))), pi_1 (S,x) are_isomorphic ) by Lm16, TOPALG_3:33, TOPREALB:11;
hence INT.Group , pi_1 (S,x) are_isomorphic by GROUP_6:67; :: thesis: verum