hereby :: thesis: ( ex r being Real ex x being Element of X st
( 0 < r & V c= Ball (x,r) ) implies V is bounded )

assume A1: V is bounded ; :: thesis: ex s being Real ex x being Element of X st
( 0 < s & V c= Ball (x,s) )

per cases ( V <> {} or V = {} ) ;

suppose V <> {} ; :: thesis: ex s being Real ex x being Element of X st
( 0 < s & V c= Ball (x,s) )

then consider x being Element of X such that
A2: x in V by SUBSET_1:4;
consider r being Real such that
A3: 0 < r and
A4: for x, y being Element of X st x in V & y in V holds
dist (x,y) <= r by A1;
reconsider dr = 2 * r as Real ;
take s = dr; :: thesis: ex x being Element of X st
( 0 < s & V c= Ball (x,s) )
take x = x; :: thesis: ( 0 < s & V c= Ball (x,s) )
thus 0 < s by A3, XREAL_1:129; :: thesis: V c= Ball (x,s)
thus V c= Ball (x,s) :: thesis: verum

proof

let u be object ; :: according to TARSKI:def 3 :: thesis: ( not u in V or u in Ball (x,s) )
assume A5: u in V ; :: thesis: u in Ball (x,s)
then reconsider v = u as Element of X ;
A6: 1 * r < s by A3, XREAL_1:68;
dist (x,v) <= r by A4, A2, A5;
then dist (x,v) < s by A6, XXREAL_0:2;
hence u in Ball (x,s) by METRIC_1:11; :: thesis: verum

end;

end;

suppose A7: V = {} ; :: thesis: ex r being Real ex x being Element of X st
( 0 < r & V c= Ball (x,r) )

set x = the Element of X;
reconsider jd = 1 / 2 as Real ;
take r = jd; :: thesis: ex x being Element of X st
( 0 < r & V c= Ball (x,r) )
take x = the Element of X; :: thesis: ( 0 < r & V c= Ball (x,r) )
thus ( 0 < r & V c= Ball (x,r) ) by A7; :: thesis: verum

end;

end;

end;

given r being Real, x being Element of X such that A8: 0 < r and
A9: V c= Ball (x,r) ; :: thesis: V is bounded
take 2 * r ; :: according to TBSP_1:def 7 :: thesis: ( not 2 * r <= 0 & ( for b₁, b₂ being Element of the carrier of X holds
( not b₁ in V or not b₂ in V or dist (b₁,b₂) <= 2 * r ) ) )
thus 2 * r > 0 by A8, XREAL_1:129; :: thesis: for b₁, b₂ being Element of the carrier of X holds
( not b₁ in V or not b₂ in V or dist (b₁,b₂) <= 2 * r )
let z, y be Element of X; :: thesis: ( not z in V or not y in V or dist (z,y) <= 2 * r )
assume A10: z in V ; :: thesis: ( not y in V or dist (z,y) <= 2 * r )
assume y in V ; :: thesis: dist (z,y) <= 2 * r
then A11: dist (x,y) < r by A9, METRIC_1:11;
dist (x,z) < r by A9, A10, METRIC_1:11;
then A12: (dist (z,x)) + (dist (x,y)) <= r + r by A11, XREAL_1:7;
dist (z,y) <= (dist (z,x)) + (dist (x,y)) by METRIC_1:4;
hence dist (z,y) <= 2 * r by A12, XXREAL_0:2; :: thesis: verum