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