let r be Real; :: 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 object ; :: 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;
A2: r + 0 < r + 1 by XREAL_1:8;
dist (x,Y) <= r by A1, METRIC_1:12;
then dist (x,Y) < r + 1 by A2, XXREAL_0:2;
hence y in Ball (x,(r + 1)) by METRIC_1:11; :: thesis: verum

end;

hence cl_Ball (x,r) is bounded by TBSP_1:14; :: thesis: verum