( a is Real & b is Real ) by XREAL_0:def 1;
hence [.a,b.] is closed-interval Subset of REAL by A1, INTEGRA1:def 1; :: thesis: verum