for a, b being Real st a <= b holds
[.a,b.] is non empty compact Subset of REAL by XXREAL_1:30;