theorem Th1: :: PCOMPS_1:1

for PM being MetrStruct
for x being Element of PM
for r, p being Real st r <= p holds
Ball (x,r) c= Ball (x,p)