:: deftheorem defines TUnitSphere MFOLD_2:def 4 :
for n being Nat holds TUnitSphere n = Tunit_circle (n + 1);