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 number , b being R_eal such that
A1: a <= b and
A2: A = [.a,b.[ by MEASURE5:def 7;
reconsider a = a as R_eal by XXREAL_0:def 1;
A3: a <= b by A1;
then sup A = b by A2, Th47;
hence A = [.(inf A),(sup A).[ by A2, A3, Th41; :: thesis: verum