let r be set ; :: thesis: for I being interval Subset of REAL st r in I & I is right_open_interval & not ( r = inf I & r = lower_bound I ) holds
r in ].(inf I),(sup I).[
let I be interval Subset of REAL; :: thesis: ( r in I & I is right_open_interval & not ( r = inf I & r = lower_bound I ) implies r in ].(inf I),(sup I).[ )
assume that
A1: r in I and
A2: I is right_open_interval ; :: thesis: ( ( r = inf I & r = lower_bound I ) or r in ].(inf I),(sup I).[ )
consider a being Real, b being R_eal such that
A3: I = [.a,b.[ by A2, MEASURE5:def 4;
a is LowerBound of I by A3, XXREAL_2:19;
then reconsider J = I as non empty real-membered bounded_below set by A1, XXREAL_2:def 9;
A4: inf J = lower_bound J ;
reconsider r1 = r as Real by A1;
A5: ( a <= r1 & r1 < b ) by A1, A3, XXREAL_1:3;
A6: a < b by A5, XXREAL_0:2;

per cases ( r1 = a or r1 <> a ) ;

suppose r1 = a ; :: thesis: ( ( r = inf I & r = lower_bound I ) or r in ].(inf I),(sup I).[ )

hence ( ( r = inf I & r = lower_bound I ) or r in ].(inf I),(sup I).[ ) by A3, A4, A5, XXREAL_2:26; :: thesis: verum

end;

suppose r1 <> a ; :: thesis: ( ( r = inf I & r = lower_bound I ) or r in ].(inf I),(sup I).[ )

then ( a < r1 & r1 < b ) by A5, XXREAL_0:1;
then ( inf I < r1 & r1 < sup I ) by A3, A6, XXREAL_2:26, XXREAL_2:31;
hence ( ( r = inf I & r = lower_bound I ) or r in ].(inf I),(sup I).[ ) by XXREAL_1:4; :: thesis: verum

end;

end;