let
a
be
ExtReal
;
:: thesis:
min
(
a
,
-infty
)
=
-infty
a
>=
-infty
by
Def5
,
Lm4
,
Lm6
;
hence
min
(
a
,
-infty
)
=
-infty
by
Def8
;
:: thesis:
verum