let PM be MetrStruct ; :: thesis: for x being Element of PM
for r, p being real number st r <= p holds
Ball x,r c= Ball x,p
let x be Element of PM; :: thesis: for r, p being real number st r <= p holds
Ball x,r c= Ball x,p
let r, p be real number ; :: 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
A3: not PM is empty by A2;
dist x,y < r by A2, METRIC_1:12;
then dist x,y < p by A1, XXREAL_0:2;
hence y in Ball x,p by A3, METRIC_1:12; :: thesis: verum

end;

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