theorem :: JORDAN2C:131

for n being Nat
for r, s being Real st r > 0 holds
for x being Element of (Euclid n) st x = 0* n holds
for A being Subset of (TOP-REAL n) st A = Ball (x,s) holds
r * A = Ball (x,(r * s)) by Lm2;