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