let PM be MetrStruct ; :: thesis: for x, y being Element of PM
for r being Real st PM is triangle & y in Ball (x,r) holds
ex p being Real st
( p > 0 & Ball (y,p) c= Ball (x,r) )
let x, y be Element of PM; :: thesis: for r being Real st PM is triangle & y in Ball (x,r) holds
ex p being Real st
( p > 0 & Ball (y,p) c= Ball (x,r) )
let r be Real; :: thesis: ( PM is triangle & y in Ball (x,r) implies ex p being Real st
( p > 0 & Ball (y,p) c= Ball (x,r) ) )
reconsider r9 = r as Real ;
assume A1: PM is triangle ; :: thesis: ( not y in Ball (x,r) or ex p being Real st
( p > 0 & Ball (y,p) c= Ball (x,r) ) )
assume A2: y in Ball (x,r) ; :: thesis: ex p being Real st
( p > 0 & Ball (y,p) c= Ball (x,r) )
then A3: dist (x,y) < r by METRIC_1:11;
A4: not PM is empty by A2;
thus ex p being Real st
( p > 0 & Ball (y,p) c= Ball (x,r) ) :: thesis: verum

proof

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

proof

let z be Element of PM; :: thesis: ( z in Ball (y,(r9 - (dist (x,y)))) implies z in Ball (x,r) )
assume z in Ball (y,(r9 - (dist (x,y)))) ; :: thesis: z in Ball (x,r)
then dist (y,z) < r9 - (dist (x,y)) by METRIC_1:11;
then A5: (dist (x,y)) + (dist (y,z)) < r by XREAL_1:20;
(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:11; :: thesis: verum

end;

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

end;