let n be non zero Nat; :: thesis: for r being positive Real
for x being Point of (TOP-REAL n) st n >= 3 holds
Tcircle (x,r) is having_trivial_Fundamental_Group
let r be positive Real; :: thesis: for x being Point of (TOP-REAL n) st n >= 3 holds
Tcircle (x,r) is having_trivial_Fundamental_Group
let x be Point of (TOP-REAL n); :: thesis: ( n >= 3 implies Tcircle (x,r) is having_trivial_Fundamental_Group )
assume A1: n >= 3 ; :: thesis: Tcircle (x,r) is having_trivial_Fundamental_Group
then n - 1 >= 3 - 1 by XREAL_1:9;
then 0 <= n - 1 by XXREAL_0:2;
then A2: (n -' 1) + 1 = (n - 1) + 1 by XREAL_0:def 2;
2 + 1 = 3 ;
then 2 <= n -' 1 by A1, NAT_D:49;
then A3: TUnitSphere (n -' 1) is having_trivial_Fundamental_Group by Th46;
A4: TUnitSphere (n -' 1) = Tunit_circle ((n -' 1) + 1) by MFOLD_2:def 4;
A5: Tunit_circle n = Tcircle ((0. (TOP-REAL n)),1) by TOPREALB:def 7;
n in NAT by ORDINAL1:def 12;
then Tcircle (x,r), Tcircle ((0. (TOP-REAL n)),1) are_homeomorphic by TOPREALB:20;
hence Tcircle (x,r) is having_trivial_Fundamental_Group by A2, A3, A4, A5, Th13; :: thesis: verum