let r be real number ; :: thesis: for M being non empty Reflexive symmetric triangle MetrStruct
for x being Element of M holds cl_Ball x,r is bounded
let M be non empty Reflexive symmetric triangle MetrStruct ; :: thesis: for x being Element of M holds cl_Ball x,r is bounded
let x be Element of M; :: thesis: cl_Ball x,r is bounded
cl_Ball x,r c= Ball x,(r + 1)

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in cl_Ball x,r or y in Ball x,(r + 1) )
assume A1: y in cl_Ball x,r ; :: thesis: y in Ball x,(r + 1)
reconsider Y = y as Point of M by A1;
( dist x,Y <= r & r + 0 < r + 1 ) by A1, METRIC_1:13, XREAL_1:10;
then dist x,Y < r + 1 by XXREAL_0:2;
hence y in Ball x,(r + 1) by METRIC_1:12; :: thesis: verum

end;

hence cl_Ball x,r is bounded by TBSP_1:19, TBSP_1:21; :: thesis: verum