let X be RealNormSpace; :: thesis: for x being Point of X
for r, s being real number st r <= s holds
Ball x,r c= Ball x,s
let x be Point of X; :: thesis: for r, s being real number st r <= s holds
Ball x,r c= Ball x,s
let r, s be real number ; :: 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:10;
then ||.(x - u).|| < (r + s) - r by XREAL_1:22;
hence u in Ball x,s ; :: thesis: verum

end;

hence Ball x,r c= Ball x,s by SUBSET_1:7; :: thesis: verum