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