theorem :: BHSP_2:46

for X being RealUnitarySpace
for x, y being Point of X
for q, r being Real st y in Ball (x,r) & r <= q holds
y in Ball (x,q)