let X be non empty Reflexive symmetric triangle MetrStruct ; :: thesis: for V being bounded Subset of X
for x being Element of X ex r being Real st
( 0 < r & V c= Ball (x,r) )
let V be bounded Subset of X; :: thesis: for x being Element of X ex r being Real st
( 0 < r & V c= Ball (x,r) )
let y be Element of X; :: thesis: ex r being Real st
( 0 < r & V c= Ball (y,r) )
consider r being Real, x being Element of X such that
A1: 0 < r and
A2: V c= Ball (x,r) by Def3;
take s = r + (dist (x,y)); :: thesis: ( 0 < s & V c= Ball (y,s) )
dist (x,y) >= 0 by METRIC_1:5;
then s >= r + 0 by XREAL_1:7;
hence 0 < s by A1; :: thesis: V c= Ball (y,s)
let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in V or e in Ball (y,s) )
assume A3: e in V ; :: thesis: e in Ball (y,s)
then reconsider e = e as Element of X ;
e in Ball (x,r) by A3, A2;
then dist (e,x) < r by METRIC_1:11;
then A4: (dist (e,x)) + (dist (x,y)) < r + (dist (x,y)) by XREAL_1:8;
dist (e,y) <= (dist (e,x)) + (dist (x,y)) by METRIC_1:4;
then dist (e,y) < r + (dist (x,y)) by A4, XXREAL_0:2;
then e in Ball (y,s) by METRIC_1:11;
hence e in Ball (y,s) ; :: thesis: verum