let I be non empty closed_interval Subset of REAL; :: thesis: ex a, b being Real st
( a <= b & I = [.a,b.] )
ex a, b being Real st I = [.a,b.] by MEASURE5:def 3;
hence ex a, b being Real st
( a <= b & I = [.a,b.] ) by XXREAL_1:29; :: thesis: verum