let
a
be
ExtReal
;
:: thesis:
(
a
in
REAL
implies
+infty
>
a
)
assume
a
in
REAL
;
:: thesis:
+infty
>
a
then
A1
:
a
<>
+infty
by
Lm0
;
+infty
>=
a
by
Def5
,
Lm3
,
Lm5
;
hence
+infty
>
a
by
A1
,
Th1
;
:: thesis:
verum