( -infty <= 0. & 0. <= +infty ) by XXREAL_0:4, XXREAL_0:5;
hence ( -infty < 0. & 0. < +infty ) by XXREAL_0:1; :: thesis: verum