let A be non empty Interval; :: thesis: ( A is closed_interval implies A = [.(inf A),(sup A).] )
assume A is closed_interval ; :: thesis: A = [.(inf A),(sup A).]
then consider a, b being real number such that
A2: ( a <= b & A = [.a,b.] ) by MEASURE5:def 6;
reconsider a = a, b = b as R_eal by XXREAL_0:def 1;
sup A = b by A2, XXREAL_2:29;
hence A = [.(inf A),(sup A).] by A2, XXREAL_2:25; :: thesis: verum