let
a
be
ExtReal
;
:: thesis:
(
a
in
REAL
or
a
=
+infty
or
a
=
-infty
)
a
in
ExtREAL
by
Def1
;
then
(
a
in
REAL
or
a
in
{
+infty
,
-infty
}
)
by
XBOOLE_0:def 3
;
hence
(
a
in
REAL
or
a
=
+infty
or
a
=
-infty
)
by
TARSKI:def 2
;
:: thesis:
verum