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
A2: ( a <= b & A = [.a,b.[ ) by MEASURE5:def 7;
reconsider a = a as R_eal by XXREAL_0:def 1;
X: a <= b by A2;
then sup A = b by A2, Def5D;
hence A = [.(inf A),(sup A).[ by A2, Def4D, X; :: thesis: verum