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;