let
x
be
ExtReal
;
:: thesis:
( not
.
x
.
=
+infty
or
x
=
+infty
or
x
=
infty
)
A1
: (
.
x
.
=
x
or

.
x
.
=

(

x
)
)
by
Def1
;
assume
.
x
.
=
+infty
;
:: thesis:
(
x
=
+infty
or
x
=
infty
)
hence
(
x
=
+infty
or
x
=
infty
)
by
A1
,
XXREAL_3:5
;
:: thesis:
verum