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;