r
<=
+infty
by
XXREAL_0:3
;
hence
not
[.
r
,
+infty
.]
is
empty
by
XXREAL_1:1
;
:: thesis:
verum