thus
.
+infty
.
=
+infty
by
Def1
;
:: thesis:
.
infty
.
=
+infty

infty
=
+infty
by
XXREAL_3:23
;
hence
.
infty
.
=
+infty
by
Def1
;
:: thesis:
verum