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;