let A be non empty Interval; :: thesis: ( A is left_open_interval implies A = ].(inf A),(sup A).] )
assume A is left_open_interval ; :: thesis: A = ].(inf A),(sup A).]
then consider a being R_eal, b being real number such that
A2: ( a <= b & A = ].a,b.] ) by MEASURE5:def 8;
reconsider b = b as R_eal by XXREAL_0:def 1;
sup A = b by A2, Def5B;
hence A = ].(inf A),(sup A).] by A2, XXREAL_1:26, XXREAL_2:27; :: thesis: verum