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
A1: A = ].a,b.[ by MEASURE5:def 2;
sup A = b by A1, XXREAL_1:28, XXREAL_2:32;
hence A = ].(inf A),(sup A).[ by A1, XXREAL_1:28, XXREAL_2:28; :: thesis: verum