let C be non empty closed_interval Subset of REAL; :: thesis: lower_bound C <= upper_bound C
set c = the Element of C;
A1: the Element of C <= upper_bound C by INTEGRA2:1;
lower_bound C <= the Element of C by INTEGRA2:1;
hence lower_bound C <= upper_bound C by A1, XXREAL_0:2; :: thesis: verum