let X be RealNormSpace; :: thesis: for x being Point of X

for r, s being Real st r <= s holds

Ball (x,r) c= Ball (x,s)

let x be Point of X; :: thesis: for r, s being Real st r <= s holds

Ball (x,r) c= Ball (x,s)

let r, s be Real; :: thesis: ( r <= s implies Ball (x,r) c= Ball (x,s) )

assume A1: r <= s ; :: thesis: Ball (x,r) c= Ball (x,s)

for u being Point of X st u in Ball (x,r) holds

u in Ball (x,s)

for r, s being Real st r <= s holds

Ball (x,r) c= Ball (x,s)

let x be Point of X; :: thesis: for r, s being Real st r <= s holds

Ball (x,r) c= Ball (x,s)

let r, s be Real; :: thesis: ( r <= s implies Ball (x,r) c= Ball (x,s) )

assume A1: r <= s ; :: thesis: Ball (x,r) c= Ball (x,s)

for u being Point of X st u in Ball (x,r) holds

u in Ball (x,s)

proof

hence
Ball (x,r) c= Ball (x,s)
; :: thesis: verum
let u be Point of X; :: thesis: ( u in Ball (x,r) implies u in Ball (x,s) )

assume u in Ball (x,r) ; :: thesis: u in Ball (x,s)

then ex uu1 being Point of X st

( u = uu1 & ||.(x - uu1).|| < r ) ;

then ||.(x - u).|| + r < r + s by A1, XREAL_1:8;

then ||.(x - u).|| < (r + s) - r by XREAL_1:20;

hence u in Ball (x,s) ; :: thesis: verum

end;assume u in Ball (x,r) ; :: thesis: u in Ball (x,s)

then ex uu1 being Point of X st

( u = uu1 & ||.(x - uu1).|| < r ) ;

then ||.(x - u).|| + r < r + s by A1, XREAL_1:8;

then ||.(x - u).|| < (r + s) - r by XREAL_1:20;

hence u in Ball (x,s) ; :: thesis: verum