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