let n be Nat; :: thesis: 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
let r, s, t be Real; :: thesis: ( 0 < s & s <= t implies 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 )
assume that
A1: 0 < s and
A2: s <= t ; :: thesis: 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
let x be Element of (Euclid n); :: thesis: ( x = 0* n implies for BA being Subset of (TOP-REAL n) st BA = Ball (x,r) holds
s * BA c= t * BA )
assume A3: x = 0* n ; :: thesis: for BA being Subset of (TOP-REAL n) st BA = Ball (x,r) holds
s * BA c= t * BA
let BA be Subset of (TOP-REAL n); :: thesis: ( BA = Ball (x,r) implies s * BA c= t * BA )
assume A4: BA = Ball (x,r) ; :: thesis: s * BA c= t * BA
let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in s * BA or e in t * BA )
assume e in s * BA ; :: thesis: e in t * BA
then consider w being Element of (TOP-REAL n) such that
A5: e = s * w and
A6: w in BA ;
w in { q where q is Element of (Euclid n) : dist (x,q) < r } by A6, A4, METRIC_1:def 14;
then consider q being Element of (Euclid n) such that
A7: w = q and
A8: dist (x,q) < r ;
set p = (s / t) * w;
A9: e = s * w by A5
.= (t * (s / t)) * w by A1, A2, XCMPLX_1:87
.= t * ((s / t) * w) by RVSUM_1:49
.= t * ((s / t) * w) ;
reconsider y = (s / t) * w as Element of (Euclid n) by EUCLID:67;
A10: dist (x,y) = (s / t) * (dist (x,q)) by A3, A7, Lm1, A1, A2, XREAL_1:139;
s / t <= 1 by A1, A2, XREAL_1:183;
then dist (x,y) <= dist (x,q) by A10, METRIC_1:5, XREAL_1:153;
then dist (x,y) < r by A8, XXREAL_0:2;
then (s / t) * w in { f where f is Element of (Euclid n) : dist (x,f) < r } ;
then (s / t) * w in BA by A4, METRIC_1:def 14;
hence e in t * BA by A9; :: thesis: verum