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 such that
A1: A = [.a,b.] by MEASURE5:def 3;
A2: a <= b by A1, XXREAL_1:29;
reconsider b = b as R_eal by XXREAL_0:def 1;
sup A = b by A1, A2, XXREAL_2:29;
hence A = [.(inf A),(sup A).] by A1, A2, XXREAL_2:25; :: thesis: verum