theorem :: JGRAPH_5:3

for a, b, d, e, r3 being Real
for PM, PM2 being non empty MetrStruct
for x being Element of PM
for x2 being Element of PM2 st d <= a & a <= b & b <= e & PM = Closed-Interval-MSpace (a,b) & PM2 = Closed-Interval-MSpace (d,e) & x = x2 holds
Ball (x,r3) c= Ball (x2,r3)