let T be non empty Reflexive symmetric triangle MetrStruct ; :: thesis: for t1 being Element of T
for r being real number holds Ball t1,r is bounded
let t1 be Element of T; :: thesis: for r being real number holds Ball t1,r is bounded
let r be real number ; :: thesis: Ball t1,r is bounded

per cases ( r <= 0 or 0 < r ) ;

suppose r <= 0 ; :: thesis: Ball t1,r is bounded

then Ball t1,r = {} T by Th17;
hence Ball t1,r is bounded ; :: thesis: verum

end;

suppose 0 < r ; :: thesis: Ball t1,r is bounded

hence Ball t1,r is bounded by Lm2; :: thesis: verum

end;

end;