let C be closed-interval Subset of REAL ; :: thesis: inf C <= sup C
consider c being Element of C;
( inf C <= c & c <= sup C ) by INTEGRA2:1;
hence inf C <= sup C by XXREAL_0:2; :: thesis: verum