let I be non empty Interval; :: thesis: ( sup I in I & inf I < sup I implies ex e being Real st
( e > 0 & [.((upper_bound I) - e),(upper_bound I).] c= I ) )
assume that
A1: sup I in I and
A2: inf I < sup I ; :: thesis: ex e being Real st
( e > 0 & [.((upper_bound I) - e),(upper_bound I).] c= I )
A3: sup I = upper_bound I by A1, Lm6;
I is non empty Subset of ExtREAL by Lm10;
then consider q being Element of ExtREAL such that
A4: ( q in I & q < sup I ) by A2, XXREAL_2:95;
reconsider q = q as Real by A4;
take e = (upper_bound I) - q; :: thesis: ( e > 0 & [.((upper_bound I) - e),(upper_bound I).] c= I )
thus e > 0 by A3, A4, XREAL_1:50; :: thesis: [.((upper_bound I) - e),(upper_bound I).] c= I
thus [.((upper_bound I) - e),(upper_bound I).] c= I :: thesis: verum

proof

per cases ( I is closed_interval or I is left_open_interval ) by A1, Lm12;

suppose I is closed_interval ; :: thesis: [.((upper_bound I) - e),(upper_bound I).] c= I

then A5: I = [.(inf I),(sup I).] by MEASURE6:17;
inf I <= q by A4, A5, XXREAL_1:1;
hence [.((upper_bound I) - e),(upper_bound I).] c= I by A3, A5, XXREAL_1:34; :: thesis: verum

end;

suppose I is left_open_interval ; :: thesis: [.((upper_bound I) - e),(upper_bound I).] c= I

then A6: I = ].(inf I),(sup I).] by MEASURE6:19;
inf I < q by A4, A6, XXREAL_1:2;
hence [.((upper_bound I) - e),(upper_bound I).] c= I by A3, A6, XXREAL_1:39; :: thesis: verum

end;

end;

end;