per
cases
(
A
<>
{}
or
A
=
{}
)
;
suppose
A1
:
A
<>
{}
;
:: thesis:
r
**
A
is
bounded_above
A
c=
REAL
by
MEMBERED:3
;
hence
r
**
A
is
bounded_above
by
A1
,
INTEGRA2:9
;
:: thesis:
verum
end;
suppose
A
=
{}
;
:: thesis:
r
**
A
is
bounded_above
hence
r
**
A
is
bounded_above
;
:: thesis:
verum
end;
end;