let V be RealUnitarySpace; :: thesis: for v being Point of V
for r, p being Real st r <= p holds
Ball (v,r) c= Ball (v,p)
let v be Point of V; :: thesis: for r, p being Real st r <= p holds
Ball (v,r) c= Ball (v,p)
let r, p be Real; :: thesis: ( r <= p implies Ball (v,r) c= Ball (v,p) )
assume A1: r <= p ; :: thesis: Ball (v,r) c= Ball (v,p)
for u being Point of V st u in Ball (v,r) holds
u in Ball (v,p)
proof
let u be Point of V; :: thesis: ( u in Ball (v,r) implies u in Ball (v,p) )
assume u in Ball (v,r) ; :: thesis: u in Ball (v,p)
then dist (v,u) < r by BHSP_2:41;
then (dist (v,u)) + r < r + p by A1, XREAL_1:8;
then dist (v,u) < (r + p) - r by XREAL_1:20;
hence u in Ball (v,p) by BHSP_2:41; :: thesis: verum
end;
hence Ball (v,r) c= Ball (v,p) ; :: thesis: verum