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

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

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

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

end;

suppose r1 <> b ; :: thesis: ( ( r = sup I & r = upper_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:27, XXREAL_2:30;
hence ( ( r = sup I & r = upper_bound I ) or r in ].(inf I),(sup I).[ ) by XXREAL_1:4; :: thesis: verum

end;

end;