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

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

then Ball (t1,r) = {} T by Th12;
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;