[.0,1.] is closed-interval by INTEGRA1:def 1;
hence not [.0,1.] is empty by INTEGRA1:2; :: thesis: verum