let A be non empty Interval; :: thesis: ( A is open_interval implies A = ].(inf A),(sup A).[ )
assume A is open_interval ; :: thesis: A = ].(inf A),(sup A).[
then consider a, b being R_eal such that
A2: ( a <= b & A = ].a,b.[ ) by MEASURE5:def 5;
sup A = b by A2, XXREAL_1:28, XXREAL_2:32;
hence A = ].(inf A),(sup A).[ by A2, XXREAL_1:28, XXREAL_2:28; :: thesis: verum