let A be non empty Interval; ( A is left_open_interval implies A = ].(inf A),(sup A).] )
assume
A is left_open_interval
; 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; verum