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