for n being Nat st n >= 2 holds
TUnitSphere n is having_trivial_Fundamental_Group