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

proof

set p = r' - (dist x,y);
A5: for z being Element of PM st z in Ball y,(r' - (dist x,y)) holds
z in Ball x,r

proof

let z be Element of PM; :: thesis:
assume z in Ball y,(r' - (dist x,y)) ; :: thesis:
then dist y,z < r' - (dist x,y) by METRIC_1:12;
then A6: (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 A6, XXREAL_0:2;
hence z in Ball x,r by A3, METRIC_1:12; :: thesis:

end;

take r' - (dist x,y) ; :: thesis:
thus r' - (dist x,y) > 0 by A4, XREAL_1:52; :: thesis:
thus Ball y,(r' - (dist x,y)) c= Ball x,r by A5, SUBSET_1:7; :: thesis:

end;