let
a
be
ExtReal
;
:: thesis:
min
(
a
,
+infty
)
=
a
a
<=
+infty
by
Def5
,
Lm3
,
Lm5
;
hence
min
(
a
,
+infty
)
=
a
by
Def8
;
:: thesis:
verum