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)

proof

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;

hence Ball (x,r) c= Ball (x,s) ; :: thesis: verum