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 Element of REAL ex x being Element of X st
( 0 < s & V c= Ball x,s )

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

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

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, TBSP_1:def 9;
consider x being Element of X such that
A5: x in V by A2, SUBSET_1:10;
take s = 2 * r; :: 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:131; :: thesis: V c= Ball x,s
thus V c= Ball x,s :: thesis: verum

proof

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

end;

end;

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

consider x being Element of X;
take r = 1 / 2; :: thesis: ex x being Element of X st
( 0 < r & V c= Ball x,r )
take x = x; :: thesis: ( 0 < r & V c= Ball x,r )
thus ( 0 < r & V c= Ball x,r ) by A8, XBOOLE_1:2; :: thesis: verum

end;

end;

end;

given r being Real, x being Element of X such that A9: 0 < r and
A10: V c= Ball x,r ; :: thesis: V is bounded
take 2 * r ; :: according to TBSP_1:def 9 :: 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 A9, XREAL_1:131; :: 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 z in V ; :: thesis: ( not y in V or dist z,y <= 2 * r )
then A11: dist x,z < r by A10, METRIC_1:12;
assume y in V ; :: thesis: dist z,y <= 2 * r
then dist x,y < r by A10, METRIC_1:12;
then A12: (dist z,x) + (dist x,y) <= r + r by A11, XREAL_1:9;
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