let A be non empty Interval; :: thesis: ( A is right_open_interval implies A = [.(inf A),(sup A).[ )
assume A is right_open_interval ; :: thesis: A = [.(inf A),(sup A).[
then consider a being Real, b being R_eal such that
A1: A = [.a,b.[ by MEASURE5:def 4;
reconsider a = a as R_eal by XXREAL_0:def 1;
A2: a <= b by A1, XXREAL_1:27;
then sup A = b by A1, Th15;
hence A = [.(inf A),(sup A).[ by A1, A2, Th11; :: thesis: verum