+infty
in
{
REAL
,
[
0
,
REAL
]
}
by
TARSKI:def 2
;
then
+infty
in
ExtREAL
by
XBOOLE_0:def 3
;
hence
+infty
is
ext-real
;
:: thesis:
verum