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:10;
then dist v,u < (r + p) - r by XREAL_1:22;
hence u in Ball v,p by BHSP_2:41; :: thesis: verum

end;

hence Ball v,r c= Ball v,p by SUBSET_1:7; :: thesis: verum