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

proof

per cases ( I is closed_interval or I is right_open_interval ) by A1, Lm11;

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

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

end;

suppose I is right_open_interval ; :: thesis: [.(lower_bound I),((lower_bound I) + e).] c= I

then A6: I = [.(inf I),(sup I).[ by MEASURE6:18;
q < sup I by A4, A6, XXREAL_1:3;
hence [.(lower_bound I),((lower_bound I) + e).] c= I by A3, A6, XXREAL_1:43; :: thesis: verum

end;

end;

end;