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