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= cl_Ball (p,r2) & Ball (p,r1) c= cl_Ball (p,r2) & 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= cl_Ball (p,r2) & Ball (p,r1) c= cl_Ball (p,r2) & Ball (p,r1) c= Ball (p,r2) )
let r1, r2 be Real; :: thesis: ( r1 <= r2 implies ( cl_Ball (p,r1) c= cl_Ball (p,r2) & Ball (p,r1) c= cl_Ball (p,r2) & Ball (p,r1) c= Ball (p,r2) ) )
assume A1: r1 <= r2 ; :: thesis: ( cl_Ball (p,r1) c= cl_Ball (p,r2) & Ball (p,r1) c= cl_Ball (p,r2) & Ball (p,r1) c= Ball (p,r2) )
thus cl_Ball (p,r1) c= cl_Ball (p,r2) :: thesis: ( Ball (p,r1) c= cl_Ball (p,r2) & Ball (p,r1) c= Ball (p,r2) )
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in cl_Ball (p,r1) or x in cl_Ball (p,r2) )
assume A2: x in cl_Ball (p,r1) ; :: thesis: x in cl_Ball (p,r2)
then reconsider y = x as Point of M ;
ex q being Element of M st
( y = q & ||.(p - q).|| <= r1 ) by A2;
then ||.(p - y).|| <= r2 by A1, XXREAL_0:2;
hence x in cl_Ball (p,r2) ; :: thesis: verum
end;
thus Ball (p,r1) c= cl_Ball (p,r2) :: thesis: Ball (p,r1) c= Ball (p,r2)
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Ball (p,r1) or x in cl_Ball (p,r2) )
assume A3: x in Ball (p,r1) ; :: thesis: x in cl_Ball (p,r2)
then reconsider y = x as Point of M ;
ex q being Element of M st
( y = q & ||.(p - q).|| < r1 ) by A3;
then ||.(p - y).|| <= r2 by A1, XXREAL_0:2;
hence x in cl_Ball (p,r2) ; :: thesis: verum
end;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Ball (p,r1) or x in Ball (p,r2) )
assume A4: x in Ball (p,r1) ; :: thesis: x in Ball (p,r2)
then reconsider y = x as Point of M ;
ex q being Element of M st
( y = q & ||.(p - q).|| < r1 ) by A4;
then ||.(p - y).|| < r2 by A1, XXREAL_0:2;
hence x in Ball (p,r2) ; :: thesis: verum