let M be RealNormSpace; :: thesis: for p being Element of M
for r1, r2 being Real st r1 < r2 holds
cl_Ball (p,r1) c= Ball (p,r2)
let p be Element of M; :: thesis: for r1, r2 being Real st r1 < r2 holds
cl_Ball (p,r1) c= Ball (p,r2)
let r1, r2 be Real; :: thesis: ( r1 < r2 implies cl_Ball (p,r1) c= Ball (p,r2) )
assume A1: r1 < r2 ; :: thesis: cl_Ball (p,r1) c= Ball (p,r2)
assume not cl_Ball (p,r1) c= Ball (p,r2) ; :: thesis: contradiction
then consider x being object such that
A2: ( x in cl_Ball (p,r1) & not x in Ball (p,r2) ) by TARSKI:def 3;
reconsider x = x as Point of M by A2;
A3: ex q being Element of M st
( x = q & ||.(p - q).|| <= r1 ) by A2;
r2 <= ||.(p - x).|| by A2;
hence contradiction by A1, A3, XXREAL_0:2; :: thesis: verum