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;