for n being Nat
for r, s, t being Real st 0 < s & s <= t holds
for x being Element of (Euclid n) st x = 0* n holds
for BA being Subset of (TOP-REAL n) st BA = Ball (x,r) holds
s * BA c= t * BA by Lm3;