let
a
be
ExtReal
;
:: thesis:
(
a
in
REAL
implies
-infty
<
a
)
-infty
<=
a
by
Def5
,
Lm4
,
Lm6
;
hence
(
a
in
REAL
implies
-infty
<
a
)
by
Th1
,
Th11
;
:: thesis:
verum