let PM be MetrStruct ; :: thesis: for x being Element of PM
for r, p being Real st r <= p holds
Ball (x,r) c= Ball (x,p)
let x be Element of PM; :: thesis: for r, p being Real st r <= p holds
Ball (x,r) c= Ball (x,p)
let r, p be Real; :: thesis: ( r <= p implies Ball (x,r) c= Ball (x,p) )
assume A1: r <= p ; :: thesis: Ball (x,r) c= Ball (x,p)
for y being Element of PM st y in Ball (x,r) holds
y in Ball (x,p)

proof

let y be Element of PM; :: thesis: ( y in Ball (x,r) implies y in Ball (x,p) )
assume A2: y in Ball (x,r) ; :: thesis: y in Ball (x,p)
then dist (x,y) < r by METRIC_1:11;
then A3: dist (x,y) < p by A1, XXREAL_0:2;
not PM is empty by A2;
hence y in Ball (x,p) by A3, METRIC_1:11; :: thesis: verum

end;

hence Ball (x,r) c= Ball (x,p) ; :: thesis: verum