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