let
e
be
TheEvent
of
r
;
:: thesis:
not
e
is
empty
per
cases
(
r
<=
0
or
r
>
0
)
;
suppose
r
<=
0
;
:: thesis:
not
e
is
empty
then
e
=
[.
0
,
+infty
.[
by
Def555
;
hence
not
e
is
empty
by
XXREAL_1:3
;
:: thesis:
verum
end;
suppose
A1
:
r
>
0
;
:: thesis:
not
e
is
empty
then
e
=
[.
0
,
r
.]
by
Def555
;
hence
not
e
is
empty
by
A1
,
XXREAL_1:1
;
:: thesis:
verum
end;
end;