let PM be MetrStruct ; :: thesis:
let y, x be Element of PM; :: thesis:
let r be real number ; :: thesis:
reconsider r9 = r as Real by XREAL_0:def 1;
assume A1: PM is triangle ; :: thesis:
assume A2: y in Ball x,r ; :: thesis:
then A3: dist x,y < r by METRIC_1:12;
A4: not PM is empty by A2;
thus ex p being Real st
( p > 0 & Ball y,p c= Ball x,r ) :: thesis:

set p = r9 - (dist x,y);
take r9 - (dist x,y) ; :: thesis:
thus r9 - (dist x,y) > 0 by A3, XREAL_1:52; :: thesis:
for z being Element of PM st z in Ball y,(r9 - (dist x,y)) holds
z in Ball x,r

let z be Element of PM; :: thesis:
assume z in Ball y,(r9 - (dist x,y)) ; :: thesis:
then dist y,z < r9 - (dist x,y) by METRIC_1:12;
then A5: (dist x,y) + (dist y,z) < r by XREAL_1:22;
(dist x,y) + (dist y,z) >= dist x,z by A1, METRIC_1:4;
then dist x,z < r by A5, XXREAL_0:2;
hence z in Ball x,r by A4, METRIC_1:12; :: thesis:

end;

hence Ball y,(r9 - (dist x,y)) c= Ball x,r by SUBSET_1:7; :: thesis:

end;