let r be set ; :: thesis: for I being interval Subset of REAL st r in I & I is closed_interval & not ( r = inf I & r = lower_bound I ) & 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 closed_interval & not ( r = inf I & r = lower_bound I ) & 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 closed_interval ; :: thesis: ( ( r = inf I & r = lower_bound I ) or ( r = sup I & r = upper_bound I ) or r in ].(inf I),(sup I).[ )
consider a, b being Real such that
A3: I = [.a,b.] by A2, MEASURE5:def 3;
A4: I = [.(lower_bound I),(upper_bound I).] by A1, A2, INTEGRA1:4;
reconsider r1 = r as Real by A1;
A5: ( a <= r1 & r1 <= b ) by A1, A3, XXREAL_1:1;

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

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

hence ( ( r = inf I & r = lower_bound I ) or ( r = sup I & r = upper_bound I ) or r in ].(inf I),(sup I).[ ) by A1, A2, A3, A4, A5, INTEGRA1:5, XXREAL_2:25; :: thesis: verum

end;

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

hence ( ( r = inf I & r = lower_bound I ) or ( r = sup I & r = upper_bound I ) or r in ].(inf I),(sup I).[ ) by A1, A2, A3, A4, A5, INTEGRA1:5, XXREAL_2:29; :: thesis: verum

end;

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

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

end;

end;