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