assume
+infty
in
[:
{
0
}
,
REAL+
:]
;
:: thesis:
contradiction
then
+infty
in
REAL+
\/
[:
{
0
}
,
REAL+
:]
by
XBOOLE_0:def 3
;
then
+infty
in
REAL
by
Lm2
,
ZFMISC_1:56
;
hence
contradiction
by
Lm0
;
:: thesis:
verum