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