:: deftheorem defines Tunit_ball MFOLD_1:def 3 :
for n being Nat holds Tunit_ball n = Tball ((0. (TOP-REAL n)),1);