( a is Real & b is Real ) by XREAL_0:def 1;
hence [.a,b.] is non empty closed_interval Subset of REAL by A1, MEASURE5:14; :: thesis: verum